Library HoTT.Pointed.pTrunc
Require Import Basics Types WildCat Truncations
Pointed.Core Pointed.pEquiv Pointed.Loops Pointed.pModality.
Local Open Scope pointed_scope.
Pointed.Core Pointed.pEquiv Pointed.Loops Pointed.pModality.
Local Open Scope pointed_scope.
Truncations of pointed types
We specialize pto and pequiv_pto from pModalities.v to truncations.
Definition ptr {n : trunc_index} {A : pType} : A ->* pTr n A
:= pto (Tr n) _.
Definition pequiv_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.
Definition pTr_rec n {X Y : pType} `{IsTrunc n Y} (f : X ->* Y)
: pTr n X ->* Y
:= Build_pMap (pTr n X) Y (Trunc_rec f) (point_eq f).
: 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 _.
Definition pTr_rec_beta_path n {X Y : pType} `{IsTrunc n Y} (f : X ->* Y)
: pTr_rec n f o× ptr = f.
Proof.
unfold pTr_rec, "o*"; cbn.
(* Since f is definitionally equal to Build_pMap _ _ f (point_eq f), this works: *)
apply (ap (Build_pMap _ _ f)).
apply concat_1p.
Defined.
: pTr_rec n f o× ptr = f.
Proof.
unfold pTr_rec, "o*"; cbn.
(* Since f is definitionally equal to Build_pMap _ _ f (point_eq f), this works: *)
apply (ap (Build_pMap _ _ f)).
apply concat_1p.
Defined.
The version with a pointed homotopy.
Definition pTr_rec_beta n {X Y : pType} `{IsTrunc n Y} (f : X ->* Y)
: pTr_rec n f o× ptr ==* f
:= phomotopy_path (pTr_rec_beta_path n f).
: pTr_rec n f o× ptr ==* f
:= phomotopy_path (pTr_rec_beta_path n f).
A pointed version of the induction principle.
Definition pTr_ind n {X : pType} {Y : pFam (pTr n X)} `{∀ x, 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).
Definition pequiv_ptr_rec `{Funext} {n} {X Y : pType} `{IsTrunc n Y}
: (pTr n X ->** Y) <~>* (X ->** Y)
:= pequiv_o_pto_O _ X Y.
(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).
Definition pequiv_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
Global Instance is0functor_ptr n : Is0Functor (pTr n).
Proof.
apply Build_Is0Functor.
intros X Y f.
exact (pTr_rec _ (ptr o× f)).
Defined.
Global Instance is1functor_ptr n : Is1Functor (pTr n).
Proof.
apply Build_Is1Functor.
- intros X Y f g p.
srapply pTr_ind; cbn.
snrapply Build_pForall.
+ cbn. exact (fun x ⇒ ap tr (p x)).
+ pointed_reduce.
exact (concat_p1 _ @ concat_p1 _ @ ap _ (concat_p1 _))^.
- intros X.
srapply Build_pHomotopy.
1: apply Trunc_rec_tr.
cbn. reflexivity.
- intros X Y Z f g.
srapply Build_pHomotopy.
1: by rapply Trunc_ind.
by pointed_reduce.
Defined.
Naturality of ptr. Note that we get a equality of pointed functions, not just a pointed homotopy.
Definition ptr_natural_path (n : trunc_index) {X Y : pType} (f : X ->* Y)
: fmap (pTr n) f o× ptr = ptr o× f
:= pTr_rec_beta_path n (ptr o× f).
: fmap (pTr n) f o× ptr = ptr o× f
:= pTr_rec_beta_path n (ptr o× f).
The version with a pointed homotopy.
Definition ptr_natural (n : trunc_index) {X Y : pType} (f : X ->* Y)
: fmap (pTr n) f o× ptr ==* ptr o× f
:= phomotopy_path (ptr_natural_path n f).
Definition ptr_functor_pconst {X Y : pType} n
: fmap (pTr n) (@pconst X Y) ==* pconst.
Proof.
srapply Build_pHomotopy.
1: by rapply Trunc_ind.
reflexivity.
Defined.
Definition pequiv_ptr_functor {X Y : pType} (n : trunc_index) (f : X <~>* Y)
: pTr n X <~>* pTr n Y
:= emap (pTr n) f.
Definition ptr_loops `{Univalence} (n : trunc_index) (A : pType)
: pTr n (loops A) <~>* loops (pTr n.+1 A).
Proof.
srapply Build_pEquiv'.
1: apply equiv_path_Tr.
reflexivity.
Defined.
Definition ptr_iterated_loops `{Univalence} (n : trunc_index)
(k : nat) (A : pType)
: pTr n (iterated_loops k A) <~>* iterated_loops k (pTr (trunc_index_inc' n k) A).
Proof.
revert A n.
induction k.
{ intros A n; cbn.
reflexivity. }
intros A n.
cbn; etransitivity.
1: apply ptr_loops.
rapply (emap loops).
apply IHk.
Defined.
Definition ptr_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. *)
Definition path_Tr_commutes (n : trunc_index) (A : Type) (a0 a1 : A) (p : a0 = a1)
: path_Tr (n:=n) (tr p) = ap tr p.
Proof.
by destruct p.
Defined.
(* ptr_loops commutes with the two ptr maps. *)
Definition ptr_loops_commutes `{Univalence} (n : trunc_index) (A : pType)
: (ptr_loops n A) o× ptr ==* fmap loops ptr.
Proof.
srapply Build_pHomotopy.
- intro p.
simpl.
refine (_ @ _).
+ apply path_Tr_commutes.
+ symmetry; refine (_ @ _).
× apply concat_1p.
× apply concat_p1.
- simpl.
reflexivity.
Defined.
: fmap (pTr n) f o× ptr ==* ptr o× f
:= phomotopy_path (ptr_natural_path n f).
Definition ptr_functor_pconst {X Y : pType} n
: fmap (pTr n) (@pconst X Y) ==* pconst.
Proof.
srapply Build_pHomotopy.
1: by rapply Trunc_ind.
reflexivity.
Defined.
Definition pequiv_ptr_functor {X Y : pType} (n : trunc_index) (f : X <~>* Y)
: pTr n X <~>* pTr n Y
:= emap (pTr n) f.
Definition ptr_loops `{Univalence} (n : trunc_index) (A : pType)
: pTr n (loops A) <~>* loops (pTr n.+1 A).
Proof.
srapply Build_pEquiv'.
1: apply equiv_path_Tr.
reflexivity.
Defined.
Definition ptr_iterated_loops `{Univalence} (n : trunc_index)
(k : nat) (A : pType)
: pTr n (iterated_loops k A) <~>* iterated_loops k (pTr (trunc_index_inc' n k) A).
Proof.
revert A n.
induction k.
{ intros A n; cbn.
reflexivity. }
intros A n.
cbn; etransitivity.
1: apply ptr_loops.
rapply (emap loops).
apply IHk.
Defined.
Definition ptr_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. *)
Definition path_Tr_commutes (n : trunc_index) (A : Type) (a0 a1 : A) (p : a0 = a1)
: path_Tr (n:=n) (tr p) = ap tr p.
Proof.
by destruct p.
Defined.
(* ptr_loops commutes with the two ptr maps. *)
Definition ptr_loops_commutes `{Univalence} (n : trunc_index) (A : pType)
: (ptr_loops n A) o× ptr ==* fmap loops ptr.
Proof.
srapply Build_pHomotopy.
- intro p.
simpl.
refine (_ @ _).
+ apply path_Tr_commutes.
+ symmetry; refine (_ @ _).
× apply concat_1p.
× apply concat_p1.
- simpl.
reflexivity.
Defined.
Pointed truncation preserves binary products.
Definition pequiv_ptr_prod (n : trunc_index) (A B : pType)
: pTr n (A × B) <~>* pTr n A × pTr n B.
Proof.
snrapply Build_pEquiv'.
1: nrapply equiv_Trunc_prod_cmp.
reflexivity.
Defined.
: pTr n (A × B) <~>* pTr n A × pTr n B.
Proof.
snrapply Build_pEquiv'.
1: nrapply equiv_Trunc_prod_cmp.
reflexivity.
Defined.
Truncatedness of pForall and pMap
Definition istrunc_pforall `{Univalence} {m n : trunc_index}
(X : pType@{u}) {iscX : IsConnected m.+1 X}
(Y : pFam@{u v} X) {istY : ∀ x, IsTrunc (n +2+ m) (Y x)}
: IsTrunc@{w} n (pForall X Y).
Proof.
nrapply (istrunc_equiv_istrunc _ (equiv_extension_along_pforall@{v w u} Y)).
rapply (istrunc_extension_along_conn (n:=m) _ Y (HP:=istY)).
Defined.
(X : pType@{u}) {iscX : IsConnected m.+1 X}
(Y : pFam@{u v} X) {istY : ∀ x, IsTrunc (n +2+ m) (Y x)}
: IsTrunc@{w} n (pForall X Y).
Proof.
nrapply (istrunc_equiv_istrunc _ (equiv_extension_along_pforall@{v w u} 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.
Definition istrunc_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).
`{!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.
Definition contr_pmap_isconnected_inO `{Funext} (O : ReflectiveSubuniverse)
(X : pType) `{IsConnected O X} (Y : pType) `{In O Y}
: Contr (X ->* Y).
Proof.
srapply (contr_equiv' ([O X, _] ->* Y)).
rapply pequiv_o_pto_O.
Defined.
(X : pType) `{IsConnected O X} (Y : pType) `{In O Y}
: Contr (X ->* Y).
Proof.
srapply (contr_equiv' ([O X, _] ->* Y)).
rapply pequiv_o_pto_O.
Defined.
Every pointed type is (-1)-connected.
Global Instance is_minus_one_connected_pointed (X : pType)
: IsConnected (Tr (-1)) X
:= contr_inhabited_hprop _ (tr pt).
: IsConnected (Tr (-1)) X
:= contr_inhabited_hprop _ (tr pt).