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]
LocalOpen Scope pointed_scope.(** * Truncations of pointed types *)(** TODO: Many things here can be generalized to any modality or any reflective subuniverse, and could be moved to pModality.v *)DefinitionpTr (n : trunc_index) (A : pType) : pType
:= [Tr n A, _].(** We specialize [pto] and [pequiv_pto] from pModalities.v to truncations. *)Definitionptr {n : trunc_index} {A : pType} : A ->* pTr n A
:= pto (Tr n) _.Definitionpequiv_ptr {n : trunc_index} {A : pType} `{IsTrunc n A}
: A <~>* pTr n A := @pequiv_pto (Tr n) A _.(** We could specialize [pO_rec] to give the following result, but since maps induced by truncation-recursion compute on elements of the form [tr _], we can give a better proof of pointedness than the one coming from [pO_rec]. *)DefinitionpTr_recn {XY : pType} `{IsTrunc n Y} (f : X ->* Y)
: pTr n X ->* Y
:= Build_pMap (pTr n X) Y (Trunc_rec f) (point_eq f).(** Note that we get an equality of pointed functions here, without Funext, while [pO_rec_beta] only gives a pointed homotopy. This is because [pTr_rec] computes on elements of the form [tr _]. *)
n: trunc_index X, Y: pType IsTrunc0: IsTrunc n Y f: X ->* Y
pTr_rec n f o* ptr = f
n: trunc_index X, Y: pType IsTrunc0: IsTrunc n Y f: X ->* Y
pTr_rec n f o* ptr = f
n: trunc_index X, Y: pType IsTrunc0: IsTrunc n Y f: X ->* Y
Build_pMap X Y (funx : X => f x) (1 @ point_eq f) = f
(* Since [f] is definitionally equal to [Build_pMap _ _ f (point_eq f)], this works: *)
n: trunc_index X, Y: pType IsTrunc0: IsTrunc n Y f: X ->* Y
1 @ point_eq f = dpoint_eq f
apply concat_1p.Defined.(** The version with a pointed homotopy. *)DefinitionpTr_rec_betan {XY : pType} `{IsTrunc n Y} (f : X ->* Y)
: pTr_rec n f o* ptr ==* f
:= phomotopy_path (pTr_rec_beta_path n f).(** A pointed version of the induction principle. *)DefinitionpTr_indn {X : pType} {Y : pFam (pTr n X)} `{forallx, IsTrunc n (Y x)}
(f : pForall X (Build_pFam (Y o tr) (dpoint Y)))
: pForall (pTr n X) Y
:= Build_pForall (pTr n X) Y (Trunc_ind Y f) (dpoint_eq f).Definitionpequiv_ptr_rec `{Funext} {n} {X Y : pType} `{IsTrunc n Y}
: (pTr n X ->** Y) <~>* (X ->** Y)
:= pequiv_o_pto_O _ X Y.(** ** Functoriality of [pTr] *)
n: trunc_index
Is0Functor (pTr n)
n: trunc_index
Is0Functor (pTr n)
n: trunc_index
forallab : pType, (a $-> b) -> pTr n a $-> pTr n b
n: trunc_index X, Y: pType f: X $-> Y
pTr n X $-> pTr n Y
exact (pTr_rec _ (ptr o* f)).Defined.
n: trunc_index
Is1Functor (pTr n)
n: trunc_index
Is1Functor (pTr n)
n: trunc_index
forall (ab : pType) (fg : a $-> b),
f $== g -> fmap (pTr n) f $== fmap (pTr n) g
n: trunc_index
foralla : pType, fmap (pTr n) (Id a) $== Id (pTr n a)
n: trunc_index
forall (abc : pType) (f : a $-> b) (g : b $-> c),
fmap (pTr n) (g $o f) $==
fmap (pTr n) g $o fmap (pTr n) f
n: trunc_index
forall (ab : pType) (fg : a $-> b),
f $== g -> fmap (pTr n) f $== fmap (pTr n) g
n: trunc_index X, Y: pType f, g: X $-> Y p: f $== g
fmap (pTr n) f $== fmap (pTr n) g
n: trunc_index X, Y: pType f, g: X $-> Y p: f $== g
pForall X
{|
pfam_pr1 := funx : X => tr (f x) = tr (g x);
dpoint :=
(ap tr (point_eq f) @ 1) @
(ap tr (point_eq g) @ 1)^
|}
n: trunc_index X, Y: pType f, g: X $-> Y p: f $== g
forallx : X,
{|
pfam_pr1 := funx0 : X => tr (f x0) = tr (g x0);
dpoint :=
(ap tr (point_eq f) @ 1) @
(ap tr (point_eq g) @ 1)^
|} x
n: trunc_index X, Y: pType f, g: X $-> Y p: f $== g
n: trunc_index X, Y, Z: pType f: X $-> Y g: Y $-> Z
Trunc_ind
(funaa : Trunc n X =>
fmap (pTr n) (g $o f) aa =
(fmap (pTr n) g $o fmap (pTr n) f) aa)
(funa : X => 1) pt =
dpoint_eq (fmap (pTr n) (g $o f)) @
(dpoint_eq (fmap (pTr n) g $o fmap (pTr n) f))^
by pointed_reduce.Defined.(** Naturality of [ptr]. Note that we get a equality of pointed functions, not just a pointed homotopy. *)Definitionptr_natural_path (n : trunc_index) {XY : pType} (f : X ->* Y)
: fmap (pTr n) f o* ptr = ptr o* f
:= pTr_rec_beta_path n (ptr o* f).(** The version with a pointed homotopy. *)Definitionptr_natural (n : trunc_index) {XY : pType} (f : X ->* Y)
: fmap (pTr n) f o* ptr ==* ptr o* f
:= phomotopy_path (ptr_natural_path n f).
Trunc_ind
(funaa : Trunc n X =>
fmap (pTr n) pconst aa = pconst aa)
(funa : X => 1) pt =
dpoint_eq (fmap (pTr n) pconst) @ (dpoint_eq pconst)^
reflexivity.Defined.Definitionpequiv_ptr_functor {XY : pType} (n : trunc_index) (f : X <~>* Y)
: pTr n X <~>* pTr n Y
:= emap (pTr n) f.
H: Univalence n: trunc_index A: pType
pTr n (loops A) <~>* loops (pTr n.+1 A)
H: Univalence n: trunc_index A: pType
pTr n (loops A) <~>* loops (pTr n.+1 A)
H: Univalence n: trunc_index A: pType
pTr n (loops A) <~> loops (pTr n.+1 A)
H: Univalence n: trunc_index A: pType
?f pt = pt
H: Univalence n: trunc_index A: pType
equiv_path_Tr pt pt pt = pt
reflexivity.Defined.
H: Univalence n: trunc_index k: nat A: pType
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
H: Univalence n: trunc_index k: nat A: pType
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
H: Univalence k: nat
forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
H: Univalence
forall (A : pType) (n : trunc_index),
pTr n (iterated_loops 0 A) <~>*
iterated_loops 0 (pTr (trunc_index_inc' n 0) A)
H: Univalence k: nat IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k.+1 A) <~>*
iterated_loops k.+1 (pTr (trunc_index_inc' n k.+1) A)
H: Univalence
forall (A : pType) (n : trunc_index),
pTr n (iterated_loops 0 A) <~>*
iterated_loops 0 (pTr (trunc_index_inc' n 0) A)
H: Univalence A: pType n: trunc_index
pTr n A <~>* pTr n A
reflexivity.
H: Univalence k: nat IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k.+1 A) <~>*
iterated_loops k.+1 (pTr (trunc_index_inc' n k.+1) A)
H: Univalence k: nat IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A) A: pType n: trunc_index
pTr n (iterated_loops k.+1 A) <~>*
iterated_loops k.+1 (pTr (trunc_index_inc' n k.+1) A)
H: Univalence k: nat IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A) A: pType n: trunc_index
pTr n
(loops
((fix F (m : nat) : pType :=
match m with
| 0%nat => A
| (m'.+1)%nat => loops (F m')
end) k)) <~>* ?Goal
H: Univalence k: nat IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A) A: pType n: trunc_index
?Goal <~>*
loops
((fix F (m : nat) : pType :=
match m with
| 0%nat => pTr (trunc_index_inc' n.+1 k) A
| (m'.+1)%nat => loops (F m')
end) k)
H: Univalence k: nat IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A) A: pType n: trunc_index
loops
(pTr n.+1
((fix F (m : nat) : pType :=
match m with
| 0%nat => A
| (m'.+1)%nat => loops (F m')
end) k)) <~>*
loops
((fix F (m : nat) : pType :=
match m with
| 0%nat => pTr (trunc_index_inc' n.+1 k) A
| (m'.+1)%nat => loops (F m')
end) k)
H: Univalence k: nat IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A) A: pType n: trunc_index
pTr n.+1
((fix F (m : nat) : pType :=
match m with
| 0%nat => A
| (m'.+1)%nat => loops (F m')
end) k) $<~>
(fix F (m : nat) : pType :=
match m with
| 0%nat => pTr (trunc_index_inc' n.+1 k) A
| (m'.+1)%nat => loops (F m')
end) k
apply IHk.Defined.Definitionptr_loops_eq `{Univalence} (n : trunc_index) (A : pType)
: pTr n (loops A) = loops (pTr n.+1 A) :> pType
:= path_ptype (ptr_loops n A).(* This lemma generalizes a goal that appears in [ptr_loops_commutes], allowing us to prove it by path induction. *)
n: trunc_index A: Type a0, a1: A p: a0 = a1
path_Tr (tr p) = ap tr p
n: trunc_index A: Type a0, a1: A p: a0 = a1
path_Tr (tr p) = ap tr p
bydestruct p.Defined.(* [ptr_loops] commutes with the two [ptr] maps. *)
H: Univalence n: trunc_index A: pType
ptr_loops n A o* ptr ==* fmap loops ptr
H: Univalence n: trunc_index A: pType
ptr_loops n A o* ptr ==* fmap loops ptr
H: Univalence n: trunc_index A: pType
ptr_loops n A o* ptr == fmap loops ptr
H: Univalence n: trunc_index A: pType
?p pt =
dpoint_eq (ptr_loops n A o* ptr) @
(dpoint_eq (fmap loops ptr))^
H: Univalence n: trunc_index A: pType
ptr_loops n A o* ptr == fmap loops ptr
H: Univalence n: trunc_index A: pType p: loops A
(ptr_loops n A o* ptr) p = fmap loops ptr p
H: Univalence n: trunc_index A: pType p: loops A
Descent.path_OO (Tr n.+1) (Tr n) pt pt (tr p) =
1 @ (ap tr p @ 1)
((funp : loops A =>
path_Tr_commutes n A pt pt p @
(concat_1p (ap tr p @ 1) @ concat_p1 (ap tr p))^
:
(ptr_loops n A o* ptr) p = fmap loops ptr p)
:
ptr_loops n A o* ptr == fmap loops ptr) pt =
dpoint_eq (ptr_loops n A o* ptr) @
(dpoint_eq (fmap loops ptr))^
pTr n (A * B) <~> [pTr n A * pTr n B, ispointed_prod]
n: trunc_index A, B: pType
?f pt = pt
n: trunc_index A, B: pType
equiv_Trunc_prod_cmp n pt = pt
reflexivity.Defined.(** ** Truncatedness of [pForall] and [pMap] *)(** Buchholtz-van Doorn-Rijke, Theorem 4.2: Let [j >= -1] and [n >= -2]. When [X] is [j]-connected and [Y] is a pointed family of [j+k+1]-truncated types, the type of pointed sections is [n]-truncated. We formalize it with [j] replaced with a trunc index [m], and so there is a shift compared to the informal statement. This version also allows [n] to be one smaller than BvDR allow. *)
H: Univalence m, n: trunc_index X: pType iscX: IsConnected (Tr m.+1) X Y: pFam X istY: forallx : X, IsTrunc (n +2+ m) (Y x)
IsTrunc n (pForall X Y)
H: Univalence m, n: trunc_index X: pType iscX: IsConnected (Tr m.+1) X Y: pFam X istY: forallx : X, IsTrunc (n +2+ m) (Y x)
IsTrunc n (pForall X Y)
H: Univalence m, n: trunc_index X: pType iscX: IsConnected (Tr m.+1) X Y: pFam X istY: forallx : X, IsTrunc (n +2+ m) (Y x)
IsTrunc n
(Extensions.ExtensionAlong
(unit_name pt) Y (unit_name (dpoint Y)))
rapply (istrunc_extension_along_conn (n:=m) _ Y (HP:=istY)).Defined.(** From this we deduce the non-dependent version, which is Corollary 4.3 of BvDR. We include [n = -2] here as well, but in this case it is not interesting. Since [X ->* Y] is inhabited, the [n = -1] case also gives contractibility, with weaker hypotheses. *)Definitionistrunc_pmap `{Univalence} {m n : trunc_index} (X Y : pType)
`{!IsConnected m.+1 X} `{!IsTrunc (n +2+ m) Y}
: IsTrunc n (X ->* Y)
:= istrunc_pforall X (pfam_const Y).(** We can give a different proof of the [n = -1] case (with the conclusion upgraded to contractibility). This proof works for any reflective subuniverse and avoids univalence. Is it possible to generalize this to dependent functions while still avoiding univalence and/or keeping [O] a general RSU or modality? Can [istrunc_pmap] be proven without univalence? What about [istrunc_pforall]? If the [n = -2] or [n = -1] cases can be proven without univalence, the rest can be done inductively without univalence. *)
H: Funext O: ReflectiveSubuniverse X: pType H0: IsConnected O X Y: pType H1: In O Y
Contr (X ->* Y)
H: Funext O: ReflectiveSubuniverse X: pType H0: IsConnected O X Y: pType H1: In O Y
Contr (X ->* Y)
H: Funext O: ReflectiveSubuniverse X: pType H0: IsConnected O X Y: pType H1: In O Y
([O X, ispointed_O X] ->* Y) <~> (X ->* Y)
rapply pequiv_o_pto_O.Defined.(** Every pointed type is (-1)-connected. *)Global Instanceis_minus_one_connected_pointed (X : pType)
: IsConnected (Tr (-1)) X
:= contr_inhabited_hprop _ (tr pt).