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.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Require Import Pointed.Core.Require Import Pointed.Loops.Require Import Pointed.pTrunc.Require Import Pointed.pEquiv.Require Import Homotopy.Suspension.Require Import Homotopy.Freudenthal.Require Import Truncations.Require Import WildCat.Generalizable VariablesX A B f g n.LocalOpen Scope path_scope.LocalOpen Scope pointed_scope.(** ** Pointedness of [Susp] and path spaces thereof *)(** We arbitrarily choose [North] to be the point. *)Global Instanceispointed_susp {X : Type} : IsPointed (Susp X) | 0
:= North.Global Instanceispointed_path_susp `{IsPointed X}
: IsPointed (North = South :> Susp X) | 0 := merid (point X).Global Instanceispointed_path_susp' `{IsPointed X}
: IsPointed (South = North :> Susp X) | 0 := (merid (point X))^.Definitionpsusp (X : Type) : pType
:= [Susp X, _].(** ** Suspension Functor *)(** [psusp] has a functorial action. *)(** TODO: make this a displayed functor *)Global Instanceis0functor_psusp : Is0Functor psusp
:= Build_Is0Functor _ _ _ _ psusp (funXYf
=> Build_pMap (psusp X) (psusp Y) (functor_susp f) 1).(** [psusp] is a 1-functor. *)
Is1Functor psusp
Is1Functor psusp
forall (ab : Type) (fg : a $-> b),
f $== g -> fmap psusp f $== fmap psusp g
foralla : Type, fmap psusp (Id a) $== Id (psusp a)
forall (abc : Type) (f : a $-> b) (g : b $-> c),
fmap psusp (g $o f) $== fmap psusp g $o fmap psusp f
(** Action on 2-cells *)
forall (ab : Type) (fg : a $-> b),
f $== g -> fmap psusp f $== fmap psusp g
(ap (functor_susp f) (merid x))^ @
ap (functor_susp g) (merid x) = 1
X, Y: Type f, g: X -> Y p: f == g x: X
(merid (f x))^ @ merid (g x) = 1
X, Y: Type f, g: X -> Y p: f == g x: X
(merid (f x))^ @ merid (f x) = 1
apply concat_Vp.
X, Y: Type f, g: X -> Y p: f == g
(Susp_ind
(funy : Susp X =>
functor_susp f y = functor_susp g y) 11
(funx : X =>
internal_paths_rew_r
(funp : functor_susp f South =
functor_susp g South => p = 1)
(internal_paths_rew_r
(funp : functor_susp f South =
functor_susp f North =>
p @ ap (functor_susp g) (merid x) = 1)
(internal_paths_rew_r
(funp : Susp_rec North South
(funx0 : X => merid (f x0))
North =
Susp_rec North South
(funx0 : X => merid (f x0))
South =>
p^ @ ap (functor_susp g) (merid x) = 1)
(internal_paths_rew_r
(funp : Susp_rec North South
(funx0 : X => merid (g x0))
North =
Susp_rec North South
(funx0 : X => merid (g x0))
South =>
(merid (f x))^ @ p = 1)
(letp0 := p x inlety := g x inmatch
p0 in (_ = y0)
return ((merid ...)^ @ merid y0 = 1)
with
| 1 => concat_Vp (merid (f x))
end) (Susp_rec_beta_merid x))
(Susp_rec_beta_merid x))
(concat_p1 (ap (functor_susp f) (merid x))^))
(transport_paths_FlFr (merid x) 1)
:
transport
(funy : Susp X =>
functor_susp f y = functor_susp g y) (merid x)
1 = 1)
:
Build_pMap (psusp X) (psusp Y) (functor_susp f) 1 ==
Build_pMap (psusp X) (psusp Y) (functor_susp g) 1) pt =
dpoint_eq
(Build_pMap (psusp X) (psusp Y) (functor_susp f) 1) @
(dpoint_eq
(Build_pMap (psusp X) (psusp Y) (functor_susp g) 1))^
reflexivity.(** Preservation of identity. *)
foralla : Type, fmap psusp (Id a) $== Id (psusp a)
X: Type
fmap psusp (Id X) $== Id (psusp X)
X: Type
fmap psusp (Id X) == Id (psusp X)
X: Type
?p pt =
dpoint_eq (fmap psusp (Id X)) @
(dpoint_eq (Id (psusp X)))^
X: Type
fmap psusp (Id X) == Id (psusp X)
X: Type
forallx : X,
transport
(funy : Susp X =>
fmap psusp (Id X) y = Id (psusp X) y) (merid x) 1 =
1
X: Type x: X
transport
(funy : Susp X =>
fmap psusp (Id X) y = Id (psusp X) y) (merid x) 1 =
1
X: Type x: X
((ap (fmap psusp (Id X)) (ap idmap (merid x)))^ @ 1) @
merid x = 1
Susp_ind
(funy : Susp X =>
fmap psusp (Id X) y = Id (psusp X) y) 11
(funx : X =>
transport_paths_FFlr (merid x) 1 @
internal_paths_rew_r
(funp : North = Id (psusp X) South =>
((ap (fmap psusp (Id X)) p)^ @ 1) @ merid x = 1)
(internal_paths_rew_r
(funp : Susp_rec North South
(funx0 : X => merid (Id X x0)) North =
Susp_rec North South
(funx0 : X => merid (Id X x0)) South
=> (p^ @ 1) @ merid x = 1)
(internal_paths_rew_r
(funp : fmap psusp (Id X)
(Id (psusp X) South) =
fmap psusp (Id X) North =>
p @ merid x = 1)
(internal_paths_rew_r
(funp : fmap psusp (Id X)
(Id (psusp X) South) =
fmap psusp (Id X)
(Id (psusp X) South) => p = 1)
1 (concat_Vp (merid x)))
(concat_p1 (merid (Id X x))^))
(Susp_rec_beta_merid x)) (ap_idmap (merid x)))
pt =
dpoint_eq (fmap psusp (Id X)) @
(dpoint_eq (Id (psusp X)))^
reflexivity.(** Preservation of composition. *)
forall (abc : Type) (f : a $-> b) (g : b $-> c),
fmap psusp (g $o f) $== fmap psusp g $o fmap psusp f
a, b, c: Type f: a -> b g: b -> c
functor_susp (funx : a => g (f x)) ==
(funx : Susp a => functor_susp g (functor_susp f x))
a, b, c: Type f: a -> b g: b -> c
?Goal ispointed_susp = 1
a, b, c: Type f: a -> b g: b -> c
functor_susp (funx : a => g (f x)) ==
(funx : Susp a => functor_susp g (functor_susp f x))
a, b, c: Type f: a -> b g: b -> c
forallx : a,
transport
(funy : Susp a =>
functor_susp (funx0 : a => g (f x0)) y =
functor_susp g (functor_susp f y)) (merid x) 1 = 1
a, b, c: Type f: a -> b g: b -> c x: a
transport
(funy : Susp a =>
functor_susp (funx : a => g (f x)) y =
functor_susp g (functor_susp f y)) (merid x) 1 = 1
a, b, c: Type f: a -> b g: b -> c x: a
((ap (functor_susp (funx : a => g (f x))) (merid x))^ @
1) @
ap
(funx : Susp a => functor_susp g (functor_susp f x))
(merid x) = 1
a, b, c: Type f: a -> b g: b -> c x: a
ap
(funx : Susp a => functor_susp g (functor_susp f x))
(merid x) =
ap (functor_susp (funx : a => g (f x))) (merid x) @ 1
Susp_ind
(funy : Susp a =>
functor_susp (funx : a => g (f x)) y =
(funx : Susp a =>
functor_susp g (functor_susp f x)) y) 11
((funx : a =>
transport_paths_FlFr (merid x) 1 @
internal_paths_rew_r
(funp : functor_susp (funx0 : a => g (f x0))
South =
functor_susp (funx0 : a => g (f x0))
North =>
p @
ap
(funx0 : Susp a =>
functor_susp g (functor_susp f x0))
(merid x) = 1)
(moveR_Vp
(ap
(funx0 : Susp a =>
functor_susp g (functor_susp f x0))
(merid x)) 1
(ap (functor_susp (funx0 : a => g (f x0)))
(merid x))
(internal_paths_rew_r
(funp : functor_susp g
(functor_susp f North) =
functor_susp
(funx0 : a => g (f x0)) South =>
ap
(funx0 : Susp a =>
functor_susp g (functor_susp f x0))
(merid x) = p)
(internal_paths_rew_r
(funp : functor_susp g
(functor_susp f North) =
functor_susp g
(functor_susp f South) =>
p =
ap
(functor_susp
(funx0 : a => g (f x0)))
(merid x))
(internal_paths_rew_r
(funp : Susp_rec North South
(funx0 : a => merid (f x0))
North =
Susp_rec North South
(funx0 : a => merid (f x0))
South =>
ap (functor_susp g) p =
ap
(functor_susp
(funx0 : a => g (f x0)))
(merid x))
(internal_paths_rew_r
(funp : Susp_rec North South
(fun ... => merid ...)
North =
Susp_rec North South
(fun ... => merid ...)
South =>
p =
ap
(functor_susp
(fun ... => g ...))
(merid x))
(internal_paths_rew_r
(funp : Susp_rec North South
(...) North =
Susp_rec North South
(...) South =>
merid (g (...)) = p) 1
(Susp_rec_beta_merid x))
(Susp_rec_beta_merid (f x)))
(Susp_rec_beta_merid x))
(ap_compose (functor_susp f)
(functor_susp g) (merid x)))
(concat_p1
(ap
(functor_susp
(funx0 : a => g (f x0)))
(merid x)))))
(concat_p1
(ap (functor_susp (funx0 : a => g (f x0)))
(merid x))^))
:
forallx : a,
transport
(funy : Susp a =>
functor_susp (funx0 : a => g (f x0)) y =
(funx0 : Susp a =>
functor_susp g (functor_susp f x0)) y)
(merid x) 1 = 1) ispointed_susp = 1
reflexivity.Defined.(** ** Loop-Suspension Adjunction *)ModuleBook_Loop_Susp_Adjunction.(** Here is the proof of the adjunction isomorphism given in the book (6.5.4); we put it in a non-exported module for reasons discussed below. *)
H: Funext A, B: pType
(psusp A ->* B) <~> (A ->* loops B)
H: Funext A, B: pType
(psusp A ->* B) <~> (A ->* loops B)
H: Funext A, B: pType
{f : psusp A -> B & f pt = pt} <~> (A ->* loops B)
H: Funext A, B: pType
{NSm : {NS : B * B & A -> fst NS = snd NS} &
fst NSm.1 = pt} <~> (A ->* loops B)
H: Funext A, B: pType
{NSm : {NS : B * B & A -> fst NS = snd NS} &
fst NSm.1 = pt} <~>
{bp : {b : B & b = pt} & {b : B & A -> bp.1 = b}}
H: Funext A, B: pType
{bp : {b : B & b = pt} & {b : B & A -> bp.1 = b}} <~>
(A ->* loops B)
H: Funext A, B: pType
{bp : {b : B & b = pt} & {b : B & A -> bp.1 = b}} <~>
(A ->* loops B)
H: Funext A, B: pType
{b : B & A -> pt = b} <~> (A ->* loops B)
H: Funext A, B: pType
{pm : {p : B & A -> pt = p} &
{q : pt = pm.1 & pm.2 pt = q}} <~> (A ->* loops B)
make_equiv_contr_basedpaths.Defined.(** Unfortunately, with this definition it seems to be quite hard to prove that the isomorphism is natural on pointed maps. The following proof gets partway there, but ends with a pretty intractable goal. It's also quite slow, so we don't want to compile it all the time. *)(**<< Definition loop_susp_adjoint_nat_r `{Funext} (A B B' : pType) (f : psusp A ->* B) (g : B ->* B') : loop_susp_adjoint A B' (g o* f) ==* fmap loops g o* loop_susp_adjoint A B f. Proof. pointed_reduce. (* Very slow for some reason. *) srefine (Build_pHomotopy _ _). - intros a. simpl. refine (_ @ (concat_1p _)^). refine (_ @ (concat_p1 _)^). rewrite !transport_sigma. simpl. rewrite !(transport_arrow_fromconst (B := A)). rewrite !transport_paths_Fr. rewrite !ap_V, !ap_pr1_path_basedpaths. Fail rewrite ap_pp, !(ap_compose f g), ap_V. (* This line fails with current versions of the library. *) Fail reflexivity. admit. - cbn. Fail reflexivity. Abort.>> *)EndBook_Loop_Susp_Adjunction.(** Thus, instead we will construct the adjunction in terms of a unit and counit natural transformation. *)Definitionloop_susp_unit (X : pType) : X ->* loops (psusp X)
:= Build_pMap X (loops (psusp X))
(funx => merid x @ (merid (point X))^) (concat_pV _).(** By Freudenthal, we have that this map is (2n+2)-connected when [X] is (n+1)-connected. *)
(funx : X => merid (f x) @ (merid (f point0))^) ==
(funx : X =>
1 @
(ap (functor_susp f) (merid x @ (merid point0)^) @ 1))
X: Type point0: IsPointed X Y: Type f: X -> Y
?Goal point0 =
(1 @ concat_pV (merid (f point0))) @
(ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) @ 1)^
X: Type point0: IsPointed X Y: Type f: X -> Y
(funx : X => merid (f x) @ (merid (f point0))^) ==
(funx : X =>
1 @
(ap (functor_susp f) (merid x @ (merid point0)^) @ 1))
X: Type point0: IsPointed X Y: Type f: X -> Y x: X
1 @
(ap (functor_susp f) (merid x @ (merid point0)^) @ 1) =
merid (f x) @ (merid (f point0))^
X: Type point0: IsPointed X Y: Type f: X -> Y x: X
ap (functor_susp f) (merid x @ (merid point0)^) =
merid (f x) @ (merid (f point0))^
X: Type point0: IsPointed X Y: Type f: X -> Y x: X
ap (Susp_rec North South (funx : X => merid (f x)))
(merid x) @
ap (Susp_rec North South (funx : X => merid (f x)))
(merid pt)^ = merid (f x) @ (merid (f point0))^
X: Type point0: IsPointed X Y: Type f: X -> Y x: X
ap (Susp_rec North South (funx : X => merid (f x)))
(merid x) @
(ap (Susp_rec North South (funx : X => merid (f x)))
(merid pt))^ = merid (f x) @ (merid (f point0))^
((funx : X =>
(concat_1p
(ap (functor_susp f) (merid x @ (merid point0)^) @
1) @
(concat_p1
(ap (functor_susp f) (merid x @ (merid point0)^)) @
(ap_pp (Susp_rec North South (merid o f))
(merid x) (merid pt)^ @
((1 @@
ap_V
(Susp_rec North South
(funx0 : X => merid (f x0)))
(merid pt)) @
(Susp_rec_beta_merid x @@
inverse2 (Susp_rec_beta_merid pt))))))^)
:
(funx : X => merid (f x) @ (merid (f point0))^) ==
(funx : X =>
1 @
(ap (functor_susp f) (merid x @ (merid point0)^) @ 1)))
point0 =
(1 @ concat_pV (merid (f point0))) @
(ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) @ 1)^
X: Type point0: IsPointed X Y: Type f: X -> Y
(concat_1p
(ap (functor_susp f)
(merid point0 @ (merid point0)^) @ 1) @
(concat_p1
(ap (functor_susp f)
(merid point0 @ (merid point0)^)) @
(ap_pp
(Susp_rec North South (funx : X => merid (f x)))
(merid point0) (merid pt)^ @
((1 @@
ap_V
(Susp_rec North South
(funx : X => merid (f x)))
(merid pt)) @
(Susp_rec_beta_merid point0 @@
inverse2 (Susp_rec_beta_merid pt))))))^ =
(1 @ concat_pV (merid (f point0))) @
(ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) @ 1)^
X: Type point0: IsPointed X Y: Type f: X -> Y
(concat_1p
(ap (functor_susp f)
(merid point0 @ (merid point0)^) @ 1) @
(concat_p1
(ap (functor_susp f)
(merid point0 @ (merid point0)^)) @
(ap_pp
(Susp_rec North South (funx : X => merid (f x)))
(merid point0) (merid pt)^ @
((1 @@
ap_V
(Susp_rec North South
(funx : X => merid (f x)))
(merid pt)) @
(Susp_rec_beta_merid point0 @@
inverse2 (Susp_rec_beta_merid pt))))))^ @
(ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) @ 1) =
1 @ concat_pV (merid (f point0))
X: Type point0: IsPointed X Y: Type f: X -> Y
concat_pV (merid (f point0)) =
(Susp_rec_beta_merid point0 @@
inverse2 (Susp_rec_beta_merid pt))^ @
((1 @@
ap_V
(Susp_rec North South (funx : X => merid (f x)))
(merid pt))^ @
((ap_pp
(Susp_rec North South (funx : X => merid (f x)))
(merid point0) (merid pt)^)^ @
((concat_p1
(ap (functor_susp f)
(merid point0 @ (merid point0)^)))^ @
((concat_1p
(ap (functor_susp f)
(merid point0 @ (merid point0)^) @ 1))^ @
(ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) @ 1)))))
X: Type point0: IsPointed X Y: Type f: X -> Y
(Susp_rec_beta_merid point0 @@
inverse2 (Susp_rec_beta_merid pt)) @
concat_pV (merid (f point0)) =
(1 @@
ap_V
(Susp_rec North South (funx : X => merid (f x)))
(merid pt))^ @
((ap_pp
(Susp_rec North South (funx : X => merid (f x)))
(merid point0) (merid pt)^)^ @
((concat_p1
(ap (functor_susp f)
(merid point0 @ (merid point0)^)))^ @
((concat_1p
(ap (functor_susp f)
(merid point0 @ (merid point0)^) @ 1))^ @
(ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) @ 1))))
X: Type point0: IsPointed X Y: Type f: X -> Y
concat_pV
(ap
(Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x)))
(merid pt)) =
(1 @@
ap_V
(Susp_rec North South (funx : X => merid (f x)))
(merid pt))^ @
((ap_pp
(Susp_rec North South (funx : X => merid (f x)))
(merid point0) (merid pt)^)^ @
((concat_p1
(ap (functor_susp f)
(merid point0 @ (merid point0)^)))^ @
((concat_1p
(ap (functor_susp f)
(merid point0 @ (merid point0)^) @ 1))^ @
(ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) @ 1))))
X: Type point0: IsPointed X Y: Type f: X -> Y
ap_pp
(Susp_rec North South (funx : X => merid (f x)))
(merid point0) (merid pt)^ @
((1 @@
ap_V
(Susp_rec North South (funx : X => merid (f x)))
(merid pt)) @
concat_pV
(ap
(Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x)))
(merid pt))) =
(concat_p1
(ap (functor_susp f)
(merid point0 @ (merid point0)^)))^ @
((concat_1p
(ap (functor_susp f)
(merid point0 @ (merid point0)^) @ 1))^ @
(ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) @ 1))
X: Type point0: IsPointed X Y: Type f: X -> Y
ap
(ap
(Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x))))
(concat_pV (merid point0)) =
(concat_p1
(ap (functor_susp f)
(merid point0 @ (merid point0)^)))^ @
((concat_1p
(ap (functor_susp f)
(merid point0 @ (merid point0)^) @ 1))^ @
(ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) @ 1))
X: Type point0: IsPointed X Y: Type f: X -> Y
concat_1p
(ap (functor_susp f)
(merid point0 @ (merid point0)^) @ 1) @
(concat_p1
(ap (functor_susp f)
(merid point0 @ (merid point0)^)) @
ap
(ap
(Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x))))
(concat_pV (merid point0))) =
ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) @ 1
X: Type point0: IsPointed X Y: Type f: X -> Y
ap
(funp' : Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x)) North =
Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x)) North =>
1 @ p')
(ap
(funp' : Susp_rec
(GraphQuotient.GraphQuotient.gq
(inl tt)) South
(funx : X => merid (f x)) North =
Susp_rec
(GraphQuotient.GraphQuotient.gq
(inl tt)) South
(funx : X => merid (f x)) North =>
p' @ 1)
(ap
(ap
(Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x))))
(concat_pV (merid point0)))) =
ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) @ 1
X: Type point0: IsPointed X Y: Type f: X -> Y
ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) @ 1 =
ap
(funp' : Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x)) North =
Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x)) North =>
1 @ p')
(ap
(funp' : Susp_rec
(GraphQuotient.GraphQuotient.gq
(inl tt)) South
(funx : X => merid (f x)) North =
Susp_rec
(GraphQuotient.GraphQuotient.gq
(inl tt)) South
(funx : X => merid (f x)) North =>
p' @ 1)
(ap
(ap
(Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x))))
(concat_pV (merid point0))))
X: Type point0: IsPointed X Y: Type f: X -> Y
ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (functor_susp f) p @ 1))
(concat_pV (merid point0)) =
ap
(funp' : Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x)) North =
Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x)) North =>
1 @ p')
(ap
(funp' : Susp_rec
(GraphQuotient.GraphQuotient.gq
(inl tt)) South
(funx : X => merid (f x)) North =
Susp_rec
(GraphQuotient.GraphQuotient.gq
(inl tt)) South
(funx : X => merid (f x)) North =>
p' @ 1)
(ap
(ap
(Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x))))
(concat_pV (merid point0))))
X: Type point0: IsPointed X Y: Type f: X -> Y
ap
(funp' : Susp_rec North South
(funx : X => merid (f x)) North =
Susp_rec North South
(funx : X => merid (f x)) North =>
1 @ p')
(ap
(funp' : North = North =>
ap
(Susp_rec North South
(funx : X => merid (f x))) p' @ 1)
(concat_pV (merid pt))) =
ap
(funp' : Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x)) North =
Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x)) North =>
1 @ p')
(ap
(funp' : Susp_rec
(GraphQuotient.GraphQuotient.gq
(inl tt)) South
(funx : X => merid (f x)) North =
Susp_rec
(GraphQuotient.GraphQuotient.gq
(inl tt)) South
(funx : X => merid (f x)) North =>
p' @ 1)
(ap
(ap
(Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x))))
(concat_pV (merid point0))))
X: Type point0: IsPointed X Y: Type f: X -> Y
ap
(funp' : North = North =>
ap
(Susp_rec North South (funx : X => merid (f x)))
p' @ 1) (concat_pV (merid pt)) =
ap
(funp' : Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x)) North =
Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x)) North =>
p' @ 1)
(ap
(ap
(Susp_rec
(GraphQuotient.GraphQuotient.gq (inl tt))
South (funx : X => merid (f x))))
(concat_pV (merid point0)))
refine (ap_compose (ap (Susp_rec North South (merid o f)))
(funp' => p' @ 1) _).Qed.Definitionloop_susp_counit (X : pType) : psusp (loops X) ->* X
:= Build_pMap (psusp (loops X)) X (Susp_rec (point X) (point X) idmap) 1.
X, Y: pType f: X ->* Y
f o* loop_susp_counit X ==*
loop_susp_counit Y o* fmap psusp (fmap loops f)
X, Y: pType f: X ->* Y
f o* loop_susp_counit X ==*
loop_susp_counit Y o* fmap psusp (fmap loops f)
X: Type point0: IsPointed X Y: Type f: X -> Y
{| pointed_fun := f; dpoint_eq := 1 |}
o* loop_susp_counit [X, point0] ==*
loop_susp_counit [Y, f point0]
o* Build_pMap (psusp (point0 = point0))
(psusp (f point0 = f point0))
(functor_susp
(funp : point0 = point0 => 1 @ (ap f p @ 1)))
1
X: Type point0: IsPointed X Y: Type f: X -> Y
(funx : Susp (point0 = point0) =>
f (Susp_rec pt pt idmap x)) ==
(funx : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp : point0 = point0 => 1 @ (ap f p @ 1)) x))
X: Type point0: IsPointed X Y: Type f: X -> Y
?Goal pt = 1
X: Type point0: IsPointed X Y: Type f: X -> Y
(funx : Susp (point0 = point0) =>
f (Susp_rec pt pt idmap x)) ==
(funx : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp : point0 = point0 => 1 @ (ap f p @ 1)) x))
X: Type point0: IsPointed X Y: Type f: X -> Y p: point0 = point0
transport
(funy : Susp (point0 = point0) =>
f (Susp_rec pt pt idmap y) =
Susp_rec pt pt idmap
(functor_susp
(funp : point0 = point0 => 1 @ (ap f p @ 1))
y)) (merid p) 1 = 1
X: Type point0: IsPointed X Y: Type f: X -> Y p: point0 = point0
(ap f (ap (Susp_rec pt pt idmap) (merid p)))^ @
ap
(funx : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp : point0 = point0 => 1 @ (ap f p @ 1))
x)) (merid p) = 1
X: Type point0: IsPointed X Y: Type f: X -> Y p: point0 = point0
ap
(funx : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp : point0 = point0 => 1 @ (ap f p @ 1))
x)) (merid p) =
ap f (ap (Susp_rec pt pt idmap) (merid p)) @ 1
X: Type point0: IsPointed X Y: Type f: X -> Y p: point0 = point0
ap (Susp_rec pt pt idmap)
(ap
(Susp_rec North South
(funx0 : point0 = point0 =>
merid (1 @ (ap f x0 @ 1))))
(merid p)) =
ap f (ap (Susp_rec pt pt idmap) (merid p)) @ 1
X: Type point0: IsPointed X Y: Type f: X -> Y p: point0 = point0
1 @ (ap f p @ 1) =
ap f (ap (Susp_rec pt pt idmap) (merid p)) @ 1
X: Type point0: IsPointed X Y: Type f: X -> Y p: point0 = point0
ap f p @ 1 =
ap f (ap (Susp_rec pt pt idmap) (merid p)) @ 1
X: Type point0: IsPointed X Y: Type f: X -> Y p: point0 = point0
ap f p = ap f (ap (Susp_rec pt pt idmap) (merid p))
X: Type point0: IsPointed X Y: Type f: X -> Y p: point0 = point0
p = ap (Susp_rec pt pt idmap) (merid p)
X: Type point0: IsPointed X Y: Type f: X -> Y p: point0 = point0
ap (Susp_rec pt pt idmap) (merid p) = p
refine (Susp_rec_beta_merid _).
X: Type point0: IsPointed X Y: Type f: X -> Y
Susp_ind
(funy : Susp (point0 = point0) =>
(funx : Susp (point0 = point0) =>
f (Susp_rec pt pt idmap x)) y =
(funx : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp : point0 = point0 => 1 @ (ap f p @ 1))
x)) y)
(1
:
(funy : Susp (point0 = point0) =>
(funx : Susp (point0 = point0) =>
f (Susp_rec pt pt idmap x)) y =
(funx : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp : point0 = point0 => 1 @ (ap f p @ 1))
x)) y) North)
(1
:
(funy : Susp (point0 = point0) =>
(funx : Susp (point0 = point0) =>
f (Susp_rec pt pt idmap x)) y =
(funx : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp : point0 = point0 => 1 @ (ap f p @ 1))
x)) y) South)
((funp : point0 = point0 =>
internal_paths_rew_r
(funp0 : f (Susp_rec pt pt idmap South) =
Susp_rec pt pt idmap
(functor_susp
(funp0 : point0 = point0 =>
1 @ (ap f p0 @ 1)) South) =>
p0 = 1)
(internal_paths_rew_r
(funp0 : f (Susp_rec pt pt idmap North) =
f (Susp_rec pt pt idmap South) =>
(p0^ @ 1) @
ap
(funx : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp1 : point0 = point0 =>
1 @ (ap f p1 @ 1)) x))
(merid p) = 1)
(internal_paths_rew_r
(funp0 : f (Susp_rec pt pt idmap South) =
f (Susp_rec pt pt idmap North) =>
p0 @
ap
(funx : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp1 : point0 = point0 =>
1 @ (ap f p1 @ 1)) x))
(merid p) = 1)
(moveR_Vp
(ap
(funx : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp0 : point0 = point0 =>
1 @ (ap f p0 @ 1)) x))
(merid p)) 1
(ap f
(ap (Susp_rec pt pt idmap) (merid p)))
(ap_compose
(Susp_rec North South
(funx0 : point0 = point0 =>
merid (1 @ (ap f x0 @ 1))))
(Susp_rec pt pt idmap)
(merid p) @
internal_paths_rew_r
(funp0 :
Susp_rec North South
(funx0 : point0 = point0 =>
merid (1 @ ...)) North =
Susp_rec North South
(funx0 : point0 = point0 =>
merid (1 @ ...)) South =>
ap (Susp_rec pt pt idmap) p0 =
ap f
(ap
(Susp_rec pt pt idmap)
(merid p)) @ 1)
(internal_paths_rew_r
(funp0 :
Susp_rec pt pt idmap North =
Susp_rec pt pt idmap South =>
p0 =
ap f
(ap
(Susp_rec pt pt idmap)
(merid p)) @ 1)
(concat_1p (ap f p @ 1) @
ap11
(ap11 1
(ap11 1
(Susp_rec_beta_merid p)^)) 1)
(Susp_rec_beta_merid
(1 @ (ap f p @ 1))))
(Susp_rec_beta_merid p)))
(concat_p1
(ap f
(ap (Susp_rec pt pt idmap) (merid p)))^))
(ap_compose (Susp_rec pt pt idmap) f
(merid p)))
(transport_paths_FlFr (merid p) 1))
:
forallx : point0 = point0,
transport
(funy : Susp (point0 = point0) =>
(funx0 : Susp (point0 = point0) =>
f (Susp_rec pt pt idmap x0)) y =
(funx0 : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp : point0 = point0 =>
1 @ (ap f p @ 1)) x0)) y)
(merid x)
(1
:
(funy : Susp (point0 = point0) =>
(funx0 : Susp (point0 = point0) =>
f (Susp_rec pt pt idmap x0)) y =
(funx0 : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp : point0 = point0 =>
1 @ (ap f p @ 1)) x0)) y) North) =
(1
:
(funy : Susp (point0 = point0) =>
(funx0 : Susp (point0 = point0) =>
f (Susp_rec pt pt idmap x0)) y =
(funx0 : Susp (point0 = point0) =>
Susp_rec pt pt idmap
(functor_susp
(funp : point0 = point0 =>
1 @ (ap f p @ 1)) x0)) y) South)) pt = 1
reflexivity.Qed.(** Now the triangle identities *)
(concat_1p
(ap (Susp_rec x x idmap) (merid 1 @ (merid 1)^) @ 1) @
(concat_p1
(ap (Susp_rec x x idmap) (merid 1 @ (merid 1)^)) @
(ap_pp (Susp_rec x x idmap) (merid 1) (merid 1)^ @
((1 @@ ap_V (Susp_rec x x idmap) (merid 1)) @
((Susp_rec_beta_merid 1 @@
inverse2 (Susp_rec_beta_merid 1)) @ 1))))) @ 1 =
ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (Susp_rec x x idmap) p @ 1))
(concat_pV (merid 1)) @ 1
X: Type x: IsPointed X
concat_1p
(ap (Susp_rec x x idmap) (merid 1 @ (merid 1)^) @ 1) @
(concat_p1
(ap (Susp_rec x x idmap) (merid 1 @ (merid 1)^)) @
(ap_pp (Susp_rec x x idmap) (merid 1) (merid 1)^ @
((1 @@ ap_V (Susp_rec x x idmap) (merid 1)) @
((Susp_rec_beta_merid 1 @@
inverse2 (Susp_rec_beta_merid 1)) @ 1)))) =
ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (Susp_rec x x idmap) p @ 1))
(concat_pV (merid 1))
X: Type x: IsPointed X
concat_1p
(ap (Susp_rec x x idmap) (merid 1 @ (merid 1)^) @ 1) @
(concat_p1
(ap (Susp_rec x x idmap) (merid 1 @ (merid 1)^)) @
(ap_pp (Susp_rec x x idmap) (merid 1) (merid 1)^ @
((1 @@ ap_V (Susp_rec x x idmap) (merid 1)) @
concat_pV (ap (Susp_rec x x idmap) (merid 1))))) =
ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (Susp_rec x x idmap) p @ 1))
(concat_pV (merid 1))
X: Type x: IsPointed X
concat_1p
(ap (Susp_rec x x idmap) (merid 1 @ (merid 1)^) @ 1) @
(concat_p1
(ap (Susp_rec x x idmap) (merid 1 @ (merid 1)^)) @
ap (ap (Susp_rec x x idmap)) (concat_pV (merid 1))) =
ap
(funp : ispointed_susp = ispointed_susp =>
1 @ (ap (Susp_rec x x idmap) p @ 1))
(concat_pV (merid 1))
X: Type x: IsPointed X
concat_1p
(ap (Susp_rec x x idmap) (merid 1 @ (merid 1)^) @ 1) @
(concat_p1
(ap (Susp_rec x x idmap) (merid 1 @ (merid 1)^)) @
ap (ap (Susp_rec x x idmap)) (concat_pV (merid 1))) =
ap (concat 1)
(ap
(funp : Susp_rec x x idmap ispointed_susp = x =>
p @ 1)
(ap (ap (Susp_rec x x idmap))
(concat_pV (merid 1))))
X: Type x: IsPointed X
concat_p1
(ap (Susp_rec x x idmap) (merid 1 @ (merid 1)^)) @
ap (ap (Susp_rec x x idmap)) (concat_pV (merid 1)) =
ap
(funp : Susp_rec x x idmap ispointed_susp = x =>
p @ 1)
(ap (ap (Susp_rec x x idmap)) (concat_pV (merid 1)))