Built with
Alectryon , running Coq+SerAPI v8.18.0+0.18.3. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
(** * Exponential laws about products and sums in exponents *)
Require Import Functor.Core.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done ]
Require Import Category.Sum Functor.Sum.
Require Import Functor.Paths.
Require Import Functor.Identity Functor.Composition.Core.
Require Import Types.Prod ExponentialLaws.Tactics.
Require Import ExponentialLaws.Law2.Functors.
Set Universe Polymorphism .
Set Implicit Arguments .
Generalizable All Variables .
Set Asymmetric Patterns .
Local Open Scope functor_scope.
(** ** [yⁿ⁺ᵐ ≅ yⁿ × yᵐ] *)
Section Law2 .
Context `{Funext}.
Variables D C1 C2 : PreCategory.
Lemma helper1 (c : Functor C1 D * Functor C2 D)
: ((1 o (Basics.Overture.fst c + Basics.Overture.snd c) o inl C1 C2)%functor,
(1 o (Basics.Overture.fst c + Basics.Overture.snd c) o inr C1 C2)%functor)%core = c.H : Funext D, C1, C2 : PreCategory c : Functor C1 D * Functor C2 D
(1 o (fst c + snd c) o inl C1 C2,
1 o (fst c + snd c) o inr C1 C2) = c
Proof .H : Funext D, C1, C2 : PreCategory c : Functor C1 D * Functor C2 D
(1 o (fst c + snd c) o inl C1 C2,
1 o (fst c + snd c) o inr C1 C2) = c
apply path_prod; simpl ;
path_functor.
Defined .
Lemma helper2_helper (c : Functor (C1 + C2) D) x
: (1 o c o inl C1 C2 + 1 o c o inr C1 C2) x = c x.H : Funext D, C1, C2 : PreCategory c : Functor (C1 + C2) D x : (C1 + C2)%category
((1 o c o inl C1 C2 + 1 o c o inr C1 C2) _0 x)%object =
(c _0 x)%object
Proof .H : Funext D, C1, C2 : PreCategory c : Functor (C1 + C2) D x : (C1 + C2)%category
((1 o c o inl C1 C2 + 1 o c o inr C1 C2) _0 x)%object =
(c _0 x)%object
destruct x; reflexivity .
Defined .
Lemma helper2 (c : Functor (C1 + C2) D)
: 1 o c o inl C1 C2 + 1 o c o inr C1 C2 = c.H : Funext D, C1, C2 : PreCategory c : Functor (C1 + C2) D
1 o c o inl C1 C2 + 1 o c o inr C1 C2 = c
Proof .H : Funext D, C1, C2 : PreCategory c : Functor (C1 + C2) D
1 o c o inl C1 C2 + 1 o c o inr C1 C2 = c
path_functor. H : Funext D, C1, C2 : PreCategory c : Functor (C1 + C2) D
{HO
: (fun cc' : C1 + C2 =>
match cc' with
| Overture.inl c0 =>
(c _0 (Overture.inl c0))%object
| Overture.inr c' =>
(c _0 (Overture.inr c'))%object
end ) = c &
transport
(fun GO : C1 + C2 -> D =>
forall s d : C1 + C2,
match s with
| Overture.inl s0 =>
match d with
| Overture.inl d0 => morphism C1 s0 d0
| Overture.inr _ => Empty
end
| Overture.inr s0 =>
match d with
| Overture.inl _ => Empty
| Overture.inr d0 => morphism C2 s0 d0
end
end -> morphism D (GO s) (GO d)) HO
(fun s d : C1 + C2 =>
match
s as s0
return
(match s0 with
| Overture.inl s1 =>
match d with
| Overture.inl d0 => morphism C1 s1 d0
| Overture.inr _ => Empty
end
| Overture.inr s1 =>
match d with
| Overture.inl _ => Empty
| Overture.inr d0 => morphism C2 s1 d0
end
end ->
morphism D
match s0 with
| Overture.inl c0 =>
(c _0 (Overture.inl c0))%object
| Overture.inr c' =>
(c _0 (Overture.inr c'))%object
end
match d with
| Overture.inl c0 =>
(c _0 (Overture.inl c0))%object
| Overture.inr c' =>
(c _0 (Overture.inr c'))%object
end )
with
| Overture.inl cs =>
match
d as d0
return
(match d0 with
| Overture.inl d1 => morphism C1 cs d1
| Overture.inr _ => Empty
end ->
morphism D (c _0 (Overture.inl cs))%object
match d0 with
| Overture.inl c0 =>
(c _0 (Overture.inl c0))%object
| Overture.inr c' =>
(c _0 (Overture.inr c'))%object
end )
with
| Overture.inl cd =>
fun m : morphism C1 cs cd =>
(c _1 m)%morphism
| Overture.inr o =>
fun m : Empty =>
match
m
return
(morphism D
(c _0 (Overture.inl cs))%object
(c _0 (Overture.inr o))%object)
with
end
end
| Overture.inr c's =>
match
d as d0
return
(match d0 with
| Overture.inl _ => Empty
| Overture.inr d1 => morphism C2 c's d1
end ->
morphism D
(c _0 (Overture.inr c's))%object
match d0 with
| Overture.inl c0 =>
(c _0 (Overture.inl c0))%object
| Overture.inr c' =>
(c _0 (Overture.inr c'))%object
end )
with
| Overture.inl o =>
fun m : Empty =>
match
m
return
(morphism D
(c _0 (Overture.inr c's))%object
(c _0 (Overture.inl o))%object)
with
end
| Overture.inr c'd =>
fun m : morphism C2 c's c'd =>
(c _1 m)%morphism
end
end ) = morphism_of c}
(exists (path_forall _ _ (@helper2_helper c))). H : Funext D, C1, C2 : PreCategory c : Functor (C1 + C2) D
transport
(fun GO : C1 + C2 -> D =>
forall s d : C1 + C2,
match s with
| Overture.inl s0 =>
match d with
| Overture.inl d0 => morphism C1 s0 d0
| Overture.inr _ => Empty
end
| Overture.inr s0 =>
match d with
| Overture.inl _ => Empty
| Overture.inr d0 => morphism C2 s0 d0
end
end -> morphism D (GO s) (GO d))
(path_forall (1 o c o inl C1 C2 + 1 o c o inr C1 C2)
c (helper2_helper c))
(fun s d : C1 + C2 =>
match
s as s0
return
(match s0 with
| Overture.inl s1 =>
match d with
| Overture.inl d0 => morphism C1 s1 d0
| Overture.inr _ => Empty
end
| Overture.inr s1 =>
match d with
| Overture.inl _ => Empty
| Overture.inr d0 => morphism C2 s1 d0
end
end ->
morphism D
match s0 with
| Overture.inl c0 =>
(c _0 (Overture.inl c0))%object
| Overture.inr c' =>
(c _0 (Overture.inr c'))%object
end
match d with
| Overture.inl c0 =>
(c _0 (Overture.inl c0))%object
| Overture.inr c' =>
(c _0 (Overture.inr c'))%object
end )
with
| Overture.inl cs =>
match
d as d0
return
(match d0 with
| Overture.inl d1 => morphism C1 cs d1
| Overture.inr _ => Empty
end ->
morphism D (c _0 (Overture.inl cs))%object
match d0 with
| Overture.inl c0 =>
(c _0 (Overture.inl c0))%object
| Overture.inr c' =>
(c _0 (Overture.inr c'))%object
end )
with
| Overture.inl cd =>
fun m : morphism C1 cs cd =>
(c _1 m)%morphism
| Overture.inr o =>
fun m : Empty =>
match
m
return
(morphism D
(c _0 (Overture.inl cs))%object
(c _0 (Overture.inr o))%object)
with
end
end
| Overture.inr c's =>
match
d as d0
return
(match d0 with
| Overture.inl _ => Empty
| Overture.inr d1 => morphism C2 c's d1
end ->
morphism D
(c _0 (Overture.inr c's))%object
match d0 with
| Overture.inl c0 =>
(c _0 (Overture.inl c0))%object
| Overture.inr c' =>
(c _0 (Overture.inr c'))%object
end )
with
| Overture.inl o =>
fun m : Empty =>
match
m
return
(morphism D
(c _0 (Overture.inr c's))%object
(c _0 (Overture.inl o))%object)
with
end
| Overture.inr c'd =>
fun m : morphism C2 c's c'd =>
(c _1 m)%morphism
end
end ) = morphism_of c
abstract exp_laws_t.
Defined .
Lemma law
: functor D C1 C2 o inverse D C1 C2 = 1
/\ inverse D C1 C2 o functor D C1 C2 = 1 .H : Funext D, C1, C2 : PreCategory
(functor D C1 C2 o inverse D C1 C2 = 1 ) *
(inverse D C1 C2 o functor D C1 C2 = 1 )
Proof .H : Funext D, C1, C2 : PreCategory
(functor D C1 C2 o inverse D C1 C2 = 1 ) *
(inverse D C1 C2 o functor D C1 C2 = 1 )
split ;
path_functor;
[ (exists (path_forall _ _ helper1 ))
| (exists (path_forall _ _ helper2 )) ];
exp_laws_t;
unfold helper1, helper2;
exp_laws_t.
Qed .
End Law2 .