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 HFiber Factorization Truncations.Core Truncations.Connectedness HProp.Require Import Pointed.Core Pointed.pEquiv.Require Import WildCat.Require Import Spaces.Nat.Core.LocalOpen Scope pointed_scope.LocalOpen Scope path_scope.(** ** Loop spaces *)(** The type [x = x] is pointed. *)Global Instanceispointed_loopsA (a : A) : IsPointed (a = a) := 1.Definitionloops (A : pType) : pType
:= [point A = point A, 1].Definitioniterated_loops (n : nat) (A : pType) : pType
:= nat_iter n loops A.(* Inner unfolding for iterated loops *)Definitionunfold_iterated_loops (n : nat) (X : pType)
: iterated_loops n.+1 X = iterated_loops n (loops X)
:= nat_iter_succ_r _ _ _.(** The loop space decreases the truncation level by one. We don't bother making this an instance because it is automatically found by typeclass search, but we record it here in case anyone is looking for it. *)Definitionistrunc_loops {n} (A : pType) `{IsTrunc n.+1 A}
: IsTrunc n (loops A) := _.(** Similarly for connectedness. *)Definitionisconnected_loops `{Univalence} {n} (A : pType)
`{IsConnected n.+1 A} : IsConnected n (loops A) := _.
loops pUnit <~>* pUnit
loops pUnit <~>* pUnit
loops pUnit <~> pUnit
?f pt = pt
loops pUnit <~> pUnit
(fun_ : pt = pt => tt) o unit_name 1 == idmap
unit_name 1 o (fun_ : pt = pt => tt) == idmap
unit_name 1 o (fun_ : pt = pt => tt) == idmap
rapply path_contr.
equiv_adjointify (fun_ : pt = pt => tt) (unit_name 1)
((funx : Unit =>
match x as u return (tt = u) with
| tt => 1end)
:
(fun_ : pt = pt => tt) o unit_name 1 == idmap)
(path_contr 1) pt = pt
reflexivity.Defined.(** ** Functoriality of loop spaces *)(** Action on 1-cells *)
Is0Functor loops
Is0Functor loops
forallab : pType, (a $-> b) -> loops a $-> loops b
A, B: pType f: A $-> B
loops A $-> loops B
A, B: pType f: A $-> B
(point_eq f)^ @ (ap f pt @ point_eq f) = pt
A, B: pType f: A $-> B
(point_eq f)^ @ (ap f pt @ point_eq f) =
(point_eq f)^ @ point_eq f
A, B: pType f: A $-> B
ap f pt @ point_eq f = point_eq f
apply concat_1p.Defined.
Is1Functor loops
Is1Functor loops
forall (ab : pType) (fg : a $-> b),
f $== g -> fmap loops f $== fmap loops g
foralla : pType, fmap loops (Id a) $== Id (loops a)
forall (abc : pType) (f : a $-> b) (g : b $-> c),
fmap loops (g $o f) $== fmap loops g $o fmap loops f
(** Action on 2-cells *)
forall (ab : pType) (fg : a $-> b),
f $== g -> fmap loops f $== fmap loops g
A, B: pType f, g: A $-> B p: f $== g
fmap loops f $== fmap loops g
A: Type point0: IsPointed A B: Type f, g: A -> B p: forallx : A, f x = g x
Build_pMap (loops [A, point0]) (loops [B, g point0])
(funp0 : point0 = point0 =>
(p point0 @ 1)^ @ (ap f p0 @ (p point0 @ 1)))
(whiskerL (p point0 @ 1)^ (concat_1p (p point0 @ 1)) @
concat_Vp (p point0 @ 1)) ==*
Build_pMap (loops [A, point0]) (loops [B, g point0])
(funp : point0 = point0 => 1 @ (ap g p @ 1)) 1
A: Type point0: IsPointed A B: Type f, g: A -> B p: forallx : A, f x = g x
(funp0 : point0 = point0 =>
(p point0 @ 1)^ @ (ap f p0 @ (p point0 @ 1))) ==
(funp : point0 = point0 => 1 @ (ap g p @ 1))
A: Type point0: IsPointed A B: Type f, g: A -> B p: forallx : A, f x = g x
foralla : pType, fmap loops (Id a) $== Id (loops a)
A: pType
fmap loops (Id A) $== Id (loops A)
A: pType
fmap loops (Id A) == Id (loops A)
A: pType
?p pt =
dpoint_eq (fmap loops (Id A)) @
(dpoint_eq (Id (loops A)))^
A: pType
fmap loops (Id A) == Id (loops A)
A: pType p: loops A
fmap loops (Id A) p = Id (loops A) p
refine (concat_1p _ @ concat_p1 _ @ ap_idmap _).
A: pType
((funp : loops A =>
(concat_1p (ap idmap p @ 1) @ concat_p1 (ap idmap p)) @
ap_idmap p)
:
fmap loops (Id A) == Id (loops A)) pt =
dpoint_eq (fmap loops (Id A)) @
(dpoint_eq (Id (loops A)))^
reflexivity.(** Preservation of compositon. *)
forall (abc : pType) (f : a $-> b)
(g : b $-> c),
fmap loops (g $o f) $== fmap loops g $o fmap loops f
A, B, c: pType g: A $-> B f: B $-> c
fmap loops (f $o g) $== fmap loops f $o fmap loops g
A, B, c: pType g: A $-> B f: B $-> c
fmap loops (f $o g) == fmap loops f $o fmap loops g
fmap loops (f $o g) == fmap loops f $o fmap loops g
A, B, c: pType g: A $-> B f: B $-> c p: loops A
fmap loops (f $o g) p =
(fmap loops f $o fmap loops g) p
A, B, c: pType g: A $-> B f: B $-> c p: loops A
(ap f (point_eq g) @ point_eq f)^ @
(ap (funx : A => f (g x)) p @
(ap f (point_eq g) @ point_eq f)) =
(point_eq f)^ @
(ap f ((point_eq g)^ @ (ap g p @ point_eq g)) @
point_eq f)
A, B, c: pType g: A $-> B f: B $-> c p: loops A
(point_eq f)^ @
((ap f (point_eq g))^ @
(ap (funx : A => f (g x)) p @
(ap f (point_eq g) @ point_eq f))) =
(point_eq f)^ @
(ap f ((point_eq g)^ @ (ap g p @ point_eq g)) @
point_eq f)
A, B, c: pType g: A $-> B f: B $-> c p: loops A
(ap f (point_eq g))^ @
(ap (funx : A => f (g x)) p @
(ap f (point_eq g) @ point_eq f)) =
ap f ((point_eq g)^ @ (ap g p @ point_eq g)) @
point_eq f
A, B, c: pType g: A $-> B f: B $-> c p: loops A
ap f (point_eq g)^ @
(ap (funx : A => f (g x)) p @
(ap f (point_eq g) @ point_eq f)) =
ap f (point_eq g)^ @
(ap f (ap g p @ point_eq g) @ point_eq f)
A, B, c: pType g: A $-> B f: B $-> c p: loops A
ap (funx : A => f (g x)) p @
(ap f (point_eq g) @ point_eq f) =
ap f (ap g p @ point_eq g) @ point_eq f
A, B, c: pType g: A $-> B f: B $-> c p: loops A
ap (funx : A => f (g x)) p @
(ap f (point_eq g) @ point_eq f) =
ap f (ap g p) @ (ap f (point_eq g) @ point_eq f)
A, B, c: pType g: A $-> B f: B $-> c p: loops A
ap (funx : A => f (g x)) p = ap f (ap g p)
apply ap_compose.
A, B, c: pType g: A $-> B f: B $-> c
((funp : loops A =>
((inv_pp (ap f (point_eq g)) (point_eq f) @@ 1) @
concat_pp_p (point_eq f)^
(ap f (point_eq g))^
(ap (funx : A => f (g x)) p @
(ap f (point_eq g) @ point_eq f))) @
whiskerL (point_eq f)^
(((((ap_V f (point_eq g))^ @@ 1) @
whiskerL (ap f (point_eq g)^)
((whiskerR (ap_compose g f p)
(ap f (point_eq g) @ point_eq f) @
concat_p_pp (ap f (ap g p))
(ap f (point_eq g))
(point_eq f)) @
((ap_pp f (ap g p) (point_eq g))^ @@ 1))) @
concat_p_pp (ap f (point_eq g)^)
(ap f (ap g p @ point_eq g))
(point_eq f)) @
((ap_pp f (point_eq g)^ (ap g p @ point_eq g))^ @@
1))
:
fmap loops (f $o g) p =
(fmap loops f $o fmap loops g) p)
:
fmap loops (f $o g) == fmap loops f $o fmap loops g)
pt =
dpoint_eq (fmap loops (f $o g)) @
(dpoint_eq (fmap loops f $o fmap loops g))^
by pointed_reduce.Defined.(** *** Properties of loops functor *)(** Loops functor distributes over concatenation *)
X, Y: pType f: X ->* Y x, y: loops X
fmap loops f (x @ y) = fmap loops f x @ fmap loops f y
X, Y: pType f: X ->* Y x, y: loops X
fmap loops f (x @ y) = fmap loops f x @ fmap loops f y
X: Type point0: IsPointed X Y: Type f: X -> Y x, y: point0 = point0
ap f (x @ y) = ap f x @ ap f y
apply ap_pp.Defined.(** Loops is a pointed functor *)
H: Univalence n: trunc_index A, B: pType f: A ->* B C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType
loops C <~> image (Tr n) (fmap loops f)
H: Univalence n: trunc_index A, B: pType f: A ->* B C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType g:= Build_pMap A C (factor1 (image (Tr n.+1) f)) 1: A ->* C
loops C <~> image (Tr n) (fmap loops f)
H: Univalence n: trunc_index A, B: pType f: A ->* B C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType g:= Build_pMap A C (factor1 (image (Tr n.+1) f)) 1: A ->* C h:= Build_pMap C B (factor2 (image (Tr n.+1) f))
(point_eq f): C ->* B
loops C <~> image (Tr n) (fmap loops f)
H: Univalence n: trunc_index A, B: pType f: A ->* B C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType g:= Build_pMap A C (factor1 (image (Tr n.+1) f)) 1: A ->* C h:= Build_pMap C B (factor2 (image (Tr n.+1) f))
(point_eq f): C ->* B
H: Univalence n: trunc_index A, B: pType f: A ->* B C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType g:= Build_pMap A C (factor1 (image (Tr n.+1) f)) 1: A ->* C h:= Build_pMap C B (factor2 (image (Tr n.+1) f))
(point_eq f): C ->* B I:= ?Goal: Factorization (@IsConnMap (Tr n)) (@MapIn (Tr n))
(fmap loops f)
loops C <~> image (Tr n) (fmap loops f)
H: Univalence n: trunc_index A, B: pType f: A ->* B C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType g:= Build_pMap A C (factor1 (image (Tr n.+1) f)) 1: A ->* C h:= Build_pMap C B (factor2 (image (Tr n.+1) f))
(point_eq f): C ->* B
H: Univalence n: trunc_index A, B: pType f: A ->* B C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType g:= Build_pMap A C (factor1 (image (Tr n.+1) f)) 1: A ->* C h:= Build_pMap C B (factor2 (image (Tr n.+1) f))
(point_eq f): C ->* B
(funx : loops A => fmap loops h (fmap loops g x)) ==
fmap loops f
H: Univalence n: trunc_index A, B: pType f: A ->* B C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType g:= Build_pMap A C (factor1 (image (Tr n.+1) f)) 1: A ->* C h:= Build_pMap C B (factor2 (image (Tr n.+1) f))
(point_eq f): C ->* B x: loops A
fmap loops f x = fmap loops h (fmap loops g x)
H: Univalence n: trunc_index A, B: pType f: A ->* B C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType g:= Build_pMap A C (factor1 (image (Tr n.+1) f)) 1: A ->* C h:= Build_pMap C B (factor2 (image (Tr n.+1) f))
(point_eq f): C ->* B x: loops A
fmap loops f x = fmap loops (h $o g) x
H: Univalence n: trunc_index A, B: pType f: A ->* B C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType g:= Build_pMap A C (factor1 (image (Tr n.+1) f)) 1: A ->* C h:= Build_pMap C B (factor2 (image (Tr n.+1) f))
(point_eq f): C ->* B x: loops A
(point_eq f)^ @ (ap f x @ point_eq f) =
(1 @ point_eq f)^ @
(ap (funx : A => f x) x @ (1 @ point_eq f))
abstract (rewrite !concat_1p; reflexivity).
H: Univalence n: trunc_index A, B: pType f: A ->* B C:= [image (Tr n.+1) f, factor1 (image (Tr n.+1) f) pt]: pType g:= Build_pMap A C (factor1 (image (Tr n.+1) f)) 1: A ->* C h:= Build_pMap C B (factor2 (image (Tr n.+1) f))
(point_eq f): C ->* B I:= {|
intermediate := loops C;
factor1 := fmap loops g;
factor2 := fmap loops h;
fact_factors :=
(funx : loops A =>
((equiv_loops_image_subproof A B f x
:
fmap loops f x = fmap loops (h $o g) x) @
fmap_comp loops g h x)^)
:
(funx : loops A =>
fmap loops h (fmap loops g x)) == fmap loops f;
inclass1 := isconnected_fmap_loops A C g;
inclass2 := mapinO_tr_istruncmap (fmap loops h)
|}: Factorization (@IsConnMap (Tr n)) (@MapIn (Tr n))
(fmap loops f)
loops C <~> image (Tr n) (fmap loops f)
exact (path_intermediate (path_factor (O_factsys n) (fmap loops f) I
(image n (fmap loops f)))).Defined.(** Loop inversion is a pointed equivalence *)
A: pType
loops A <~>* loops A
A: pType
loops A <~>* loops A
A: pType
loops A ->* loops A
A: pType
IsEquiv ?pointed_equiv_fun
A: pType
IsEquiv (Build_pMap (loops A) (loops A) inverse 1)
apply isequiv_path_inverse.Defined.(** Loops functor preserves equivalences *)Definitionpequiv_fmap_loops {AB : pType}
: A $<~> B -> loops A $<~> loops B
:= emap loops.(** A version of [unfold_iterated_loops] that's an equivalence rather than an equality. We could get this from the equality, but it's more useful to construct it explicitly since then we can reason about it. *)
n: nat X: pType
iterated_loops n.+1 X <~>* iterated_loops n (loops X)
n: nat X: pType
iterated_loops n.+1 X <~>* iterated_loops n (loops X)
X: pType
iterated_loops 1 X <~>* iterated_loops 0 (loops X)
n: nat X: pType IHn: iterated_loops n.+1 X <~>* iterated_loops n (loops X)
iterated_loops n.+2 X <~>*
iterated_loops n.+1 (loops X)
n: nat X: pType IHn: iterated_loops n.+1 X <~>* iterated_loops n (loops X)
iterated_loops n.+2 X <~>*
iterated_loops n.+1 (loops X)
n: nat X: pType IHn: iterated_loops n.+1 X <~>* iterated_loops n (loops X)
apply pequiv_fmap_loops, IHn.Defined.(** For instance, we can prove that it's natural. *)
A, B: pType n: nat f: A ->* B
unfold_iterated_loops' n B
o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f)
o* unfold_iterated_loops' n A
A, B: pType n: nat f: A ->* B
unfold_iterated_loops' n B
o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f)
o* unfold_iterated_loops' n A
A, B: pType f: A ->* B
unfold_iterated_loops' 0 B
o* fmap (iterated_loops 1) f ==*
fmap (iterated_loops 0) (fmap loops f)
o* unfold_iterated_loops' 0 A
A, B: pType n: nat f: A ->* B IHn: unfold_iterated_loops' n B o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f) o* unfold_iterated_loops' n A
unfold_iterated_loops' n.+1 B
o* fmap (iterated_loops n.+2) f ==*
fmap (iterated_loops n.+1) (fmap loops f)
o* unfold_iterated_loops' n.+1 A
A, B: pType f: A ->* B
unfold_iterated_loops' 0 B
o* fmap (iterated_loops 1) f ==*
fmap (iterated_loops 0) (fmap loops f)
o* unfold_iterated_loops' 0 A
A, B: pType f: A ->* B
unfold_iterated_loops' 0 B
o* fmap (iterated_loops 1) f ==
fmap (iterated_loops 0) (fmap loops f)
o* unfold_iterated_loops' 0 A
A, B: pType n: nat f: A ->* B IHn: unfold_iterated_loops' n B o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f) o* unfold_iterated_loops' n A
unfold_iterated_loops' n.+1 B
o* fmap (iterated_loops n.+2) f ==*
fmap (iterated_loops n.+1) (fmap loops f)
o* unfold_iterated_loops' n.+1 A
A, B: pType n: nat f: A ->* B IHn: unfold_iterated_loops' n B o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f) o* unfold_iterated_loops' n A
fmap loops
((fix F (n : nat) :
iterated_loops n.+1 B <~>*
iterated_loops n (loops B) :=
match
n as n0
return
(iterated_loops n0.+1 B <~>*
iterated_loops n0 (loops B))
with
| 0%nat =>
pequiv_reflexive
(iterated_loops 0 (loops B))
| (n0.+1)%nat => pequiv_fmap_loops (F n0)
end) n $o
fmap
(loops o (funx : pType => nat_iter n loops x)) f) ==*
fmap (iterated_loops n.+1) (fmap loops f)
o* unfold_iterated_loops' n.+1 A
A, B: pType n: nat f: A ->* B IHn: unfold_iterated_loops' n B o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f) o* unfold_iterated_loops' n A
fmap loops
((fix F (n : nat) :
iterated_loops n.+1 B <~>*
iterated_loops n (loops B) :=
match
n as n0
return
(iterated_loops n0.+1 B <~>*
iterated_loops n0 (loops B))
with
| 0%nat =>
pequiv_reflexive
(iterated_loops 0 (loops B))
| (n0.+1)%nat => pequiv_fmap_loops (F n0)
end) n $o
fmap
(loops o (funx : pType => nat_iter n loops x)) f) ==*
fmap loops
(fmap (iterated_loops n) (fmap loops f) $o
(fix F (n : nat) :
iterated_loops n.+1 A <~>*
iterated_loops n (loops A) :=
match
n as n0
return
(iterated_loops n0.+1 A <~>*
iterated_loops n0 (loops A))
with
| 0%nat =>
pequiv_reflexive
(iterated_loops 0 (loops A))
| (n0.+1)%nat => pequiv_fmap_loops (F n0)
end) n)
A, B: pType n: nat f: A ->* B IHn: unfold_iterated_loops' n B o* fmap (iterated_loops n.+1) f ==*
fmap (iterated_loops n) (fmap loops f) o* unfold_iterated_loops' n A
(fix F (n : nat) :
iterated_loops n.+1 B <~>*
iterated_loops n (loops B) :=
match
n as n0
return
(iterated_loops n0.+1 B <~>*
iterated_loops n0 (loops B))
with
| 0%nat =>
pequiv_reflexive (iterated_loops 0 (loops B))
| (n0.+1)%nat => pequiv_fmap_loops (F n0)
end) n $o
fmap (loops o (funx : pType => nat_iter n loops x)) f $==
fmap (iterated_loops n) (fmap loops f) $o
(fix F (n : nat) :
iterated_loops n.+1 A <~>*
iterated_loops n (loops A) :=
match
n as n0
return
(iterated_loops n0.+1 A <~>*
iterated_loops n0 (loops A))
with
| 0%nat =>
pequiv_reflexive (iterated_loops 0 (loops A))
| (n0.+1)%nat => pequiv_fmap_loops (F n0)
end) n
apply IHn.Defined.(** Iterated loops preserves equivalences *)Definitionpequiv_fmap_iterated_loops {AB} n
: A <~>* B -> iterated_loops n A <~>* iterated_loops n B
:= emap (iterated_loops n).(** Loops preserves products. *)
X, Y: pType
loops (X * Y) <~>* loops X * loops Y
X, Y: pType
loops (X * Y) <~>* loops X * loops Y
X, Y: pType
loops (X * Y) <~> [loops X * loops Y, ispointed_prod]
X, Y: pType
?f pt = pt
X, Y: pType
((equiv_path_prod pt pt)^-1)%equiv pt = pt
reflexivity.Defined.(** There is a natural map from [loops (X * Y)] to [loops X * loops Y], and ideally it would definitionally underly the equivalence [loops_prod]. That's not the case, but we show that [loops_prod] is homotopic to the expected maps after projecting to each factor. *)
X, Y: pType n: nat IHn: psnd o* iterated_loops_prod X Y ==* fmap (iterated_loops n) psnd
psnd o* iterated_loops_prod X Y ==*
fmap (iterated_loops n) psnd
exact IHn.Defined.(* A dependent form of loops *)DefinitionloopsD {A} : pFam A -> pFam (loops A)
:= funPp => Build_pFam (funq : loops A => transport Pp q (dpoint Pp) = (dpoint Pp)) 1.
n: trunc_index A: pType P: pFam A H: IsTrunc_pFam n.+1 P
IsTrunc_pFam n (loopsD P)
n: trunc_index A: pType P: pFam A H: IsTrunc_pFam n.+1 P
IsTrunc_pFam n (loopsD P)
n: trunc_index A: pType P: pFam A H: IsTrunc_pFam n.+1 P a: loops A
IsTrunc n (loopsD P a)
n: trunc_index A: pType P: pFam A H: IsTrunc_pFam n.+1 P a: loops A i:= H pt: IsTrunc n.+1 (P pt)
IsTrunc n (loopsD P a)
exact _.Defined.(* psigma and loops 'commute' *)
A: pType P: pFam A
loops (psigma P) <~>* psigma (loopsD P)
A: pType P: pFam A
loops (psigma P) <~>* psigma (loopsD P)
A: pType P: pFam A
loops (psigma P) <~> psigma (loopsD P)
A: pType P: pFam A
?f pt = pt
A: pType P: pFam A
((equiv_path_sigma P pt pt)^-1)%equiv pt = pt
reflexivity.Defined.(* product and loops 'commute' *)
H: Funext A: Type F: A -> pType
loops (pproduct F) <~>* pproduct (loops o F)
H: Funext A: Type F: A -> pType
loops (pproduct F) <~>* pproduct (loops o F)
H: Funext A: Type F: A -> pType
loops (pproduct F) <~> pproduct (loops o F)
H: Funext A: Type F: A -> pType
?f pt = pt
H: Funext A: Type F: A -> pType
equiv_apD10 (funx : A => F x) pt pt pt = pt
reflexivity.Defined.(* product and iterated loops commute *)
H: Funext A: Type F: A -> pType n: nat
iterated_loops n (pproduct F) <~>*
pproduct (iterated_loops n o F)
H: Funext A: Type F: A -> pType n: nat
iterated_loops n (pproduct F) <~>*
pproduct (iterated_loops n o F)
H: Funext A: Type F: A -> pType n: nat IHn: iterated_loops n (pproduct F) <~>*
pproduct (funx : A => iterated_loops n (F x))
iterated_loops n.+1 (pproduct F) <~>*
loops
(pproduct
(funx : A =>
(fix F (m : nat) : pType :=
match m with
| 0%nat => F x
| (m'.+1)%nat => loops (F m')
end) n))
H: Funext A: Type F: A -> pType n: nat IHn: iterated_loops n (pproduct F) <~>*
pproduct (funx : A => iterated_loops n (F x))
(fix F (m : nat) : pType :=
match m with
| 0%nat => pproduct F
| (m'.+1)%nat => loops (F m')
end) n $<~>
pproduct
(funx : A =>
(fix F (m : nat) : pType :=
match m with
| 0%nat => F x
| (m'.+1)%nat => loops (F m')
end) n)
exact IHn.Defined.(* Loops neutralise sigmas when truncated *)
n: nat
forall (Aa : pType) (Pp : pFam Aa),
IsTrunc_pFam (trunc_index_inc (-2) n) Pp ->
iterated_loops n (psigma Pp) <~>* iterated_loops n Aa
n: nat
forall (Aa : pType) (Pp : pFam Aa),
IsTrunc_pFam (trunc_index_inc (-2) n) Pp ->
iterated_loops n (psigma Pp) <~>* iterated_loops n Aa
n: nat IHn: forall (Aa : pType) (Pp : pFam Aa),
IsTrunc_pFam (trunc_index_inc (-2) n) Pp ->
iterated_loops n (psigma Pp) <~>* iterated_loops n Aa A: pType P: pFam A p: IsTrunc_pFam (trunc_index_inc (-2) n.+1) P
iterated_loops n.+1 (psigma P) <~>*
iterated_loops n.+1 A
n: nat IHn: forall (Aa : pType) (Pp : pFam Aa),
IsTrunc_pFam (trunc_index_inc (-2) n) Pp ->
iterated_loops n (psigma Pp) <~>* iterated_loops n Aa A: pType P: pFam A p: IsTrunc_pFam (trunc_index_inc (-2) n.+1) P
iterated_loops n (loops (psigma P)) <~>*
iterated_loops n (loops A)
n: nat IHn: forall (Aa : pType) (Pp : pFam Aa),
IsTrunc_pFam (trunc_index_inc (-2) n) Pp ->
iterated_loops n (psigma Pp) <~>* iterated_loops n Aa A: pType P: pFam A p: IsTrunc_pFam (trunc_index_inc (-2) n.+1) P
iterated_loops n (loops (psigma P)) <~>*
iterated_loops n (psigma (loopsD P))
n: nat IHn: forall (Aa : pType) (Pp : pFam Aa),
IsTrunc_pFam (trunc_index_inc (-2) n) Pp ->
iterated_loops n (psigma Pp) <~>* iterated_loops n Aa A: pType P: pFam A p: IsTrunc_pFam (trunc_index_inc (-2) n.+1) P
loops (psigma P) $<~> psigma (loopsD P)
apply loops_psigma_commute.Defined.(* We can convert between loops in a type and loops in [Type] at that type. *)
H: Univalence A: Type
loops [Type, A] <~>* [A <~> A, 1%equiv]
H: Univalence A: Type
loops [Type, A] <~>* [A <~> A, 1%equiv]
H: Univalence A: Type
{f : loops [Type, A] <~> [A <~> A, 1%equiv] &
f pt = pt}
H: Univalence A: Type
equiv_equiv_path A A pt = pt
reflexivity.Defined.(* An iterated version. Note that the statement with "-1" substituted for [n] is [loops [Type, A] <~>* [A -> A, idmap]], which is not true in general. Compare the previous result. *)
H: Funext n: trunc_index X: Type tr_loops: forallx : X, IsTrunc n.+1 (loops [X, x]) x, y: X
IsTrunc n.+1 (x = y)
H: Funext n: trunc_index X: Type tr_loops: forallx : X, IsTrunc n.+1 (loops [X, x]) x, y: X p: x = y
forally0 : x = y, IsTrunc n (p = y0)
H: Funext n: trunc_index X: Type tr_loops: forallx : X, IsTrunc n.+1 (loops [X, x]) x: X
forally : x = x, IsTrunc n (1 = y)
nrapply tr_loops.Defined.(* 7.2.9, with [n] here meaning the same as [n-1] there. Note that [n.-1] in the statement is short for [trunc_index_pred (nat_to_trunc_index n)] which is definitionally equal to [(trunc_index_inc minus_two n).+1]. *)
H: Funext n: nat
forallA : Type,
IsTrunc n.-1 A <~>
(foralla : A, Contr (iterated_loops n [A, a]))
H: Funext n: nat
forallA : Type,
IsTrunc n.-1 A <~>
(foralla : A, Contr (iterated_loops n [A, a]))
H: Funext A: Type
IsTrunc 0%nat.-1 A <~>
(foralla : A, Contr (iterated_loops 0 [A, a]))
H: Funext n: nat IHn: forallA : Type,
IsTrunc n.-1 A <~> (foralla : A, Contr (iterated_loops n [A, a])) A: Type
IsTrunc (n.+1)%nat.-1 A <~>
(foralla : A, Contr (iterated_loops n.+1 [A, a]))
H: Funext A: Type
IsTrunc 0%nat.-1 A <~>
(foralla : A, Contr (iterated_loops 0 [A, a]))
H: Funext A: Type
IsHProp A <~> (A -> Contr A)
exact equiv_hprop_inhabited_contr.
H: Funext n: nat IHn: forallA : Type,
IsTrunc n.-1 A <~> (foralla : A, Contr (iterated_loops n [A, a])) A: Type
IsTrunc (n.+1)%nat.-1 A <~>
(foralla : A, Contr (iterated_loops n.+1 [A, a]))
H: Funext n: nat IHn: forallA : Type,
IsTrunc n.-1 A <~> (foralla : A, Contr (iterated_loops n [A, a])) A: Type
(forallx : A, IsTrunc n.-2.+1 (loops [A, x])) <~>
(foralla : A, Contr (iterated_loops n.+1 [A, a]))
H: Funext n: nat IHn: forallA : Type,
IsTrunc n.-1 A <~> (foralla : A, Contr (iterated_loops n [A, a])) A: Type
foralla : A,
(funa0 : A => IsTrunc n.-2.+1 (loops [A, a0])) a <~>
(funa0 : A => Contr (iterated_loops n.+1 [A, a0])) a
H: Funext n: nat IHn: forallA : Type,
IsTrunc n.-1 A <~> (foralla : A, Contr (iterated_loops n [A, a])) A: Type a: A
(funa : A => IsTrunc n.-2.+1 (loops [A, a])) a <~>
(funa : A => Contr (iterated_loops n.+1 [A, a])) a
H: Funext n: nat IHn: forallA : Type,
IsTrunc n.-1 A <~> (foralla : A, Contr (iterated_loops n [A, a])) A: Type a: A
((funp : loops A =>
(inv_Vp (point_eq f) (ap f p @ point_eq f) @
whiskerR
(inv_pp (ap f p) (point_eq f) @
whiskerL (point_eq f)^ (ap_V f p)^) (point_eq f)) @
concat_pp_p (point_eq f)^ (ap f (loops_inv A p))
(point_eq f))
:
loops_inv B $o fmap loops f ==
fmap loops f $o loops_inv A) pt =
dpoint_eq (loops_inv B $o fmap loops f) @
(dpoint_eq (fmap loops f $o loops_inv A))^
A: Type point0: IsPointed A B: Type f: A -> B
1 = 1
reflexivity.Defined.(** Loops on the pointed type of dependent pointed maps correspond to pointed dependent maps into a family of loops. We define this in this direction, because the forward map is pointed by reflexivity. *)
H: Funext A: pType B: A -> pType
loops (ppforall x : A, B x) <~>*
(ppforall x : A, loops (B x))
H: Funext A: pType B: A -> pType
loops (ppforall x : A, B x) <~>*
(ppforall x : A, loops (B x))
H: Funext A: pType B: A -> pType
loops (ppforall x : A, B x) <~>
(ppforall x : A, loops (B x))
H: Funext A: pType B: A -> pType
?f pt = pt
H: Funext A: pType B: A -> pType
((equiv_path_pforall (point_pforall B)
(point_pforall B))^-1)%equiv pt = pt