Timings for pTrunc.v
Require Import Basics Types WildCat Truncations
Pointed.Core Pointed.pEquiv Pointed.Loops Pointed.pModality.
Local Open 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 *)
Definition pTr (n : trunc_index) (A : pType) : pType
:= [Tr n A, _].
(** 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).
(** 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.
unfold pTr_rec, "o*"; cbn.
(* Since [f] is definitionally equal to [Build_pMap _ _ f (point_eq f)], this works: *)
apply (ap (Build_pMap _ _ f)).
(** 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).
(** A pointed version of the induction principle. *)
Definition pTr_ind n {X : pType} {Y : pFam (pTr n X)} `{forall 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.
(** ** Functoriality of [pTr] *)
Global Instance is0functor_ptr n : Is0Functor (pTr n).
exact (pTr_rec _ (ptr o* f)).
Global Instance is1functor_ptr n : Is1Functor (pTr n).
exact (fun x => ap tr (p x)).
exact (concat_p1 _ @ concat_p1 _ @ ap _ (concat_p1 _))^.
(** 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).
(** 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.
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).
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).
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.
(* [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.
symmetry; refine (_ @ _).
(** 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.
1: nrapply equiv_Trunc_prod_cmp.
(** ** 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. *)
Definition istrunc_pforall `{Univalence} {m n : trunc_index}
(X : pType@{u}) {iscX : IsConnected m.+1 X}
(Y : pFam@{u v} X) {istY : forall x, IsTrunc (n +2+ m) (Y x)}
: IsTrunc@{w} n (pForall X Y).
nrapply (istrunc_equiv_istrunc _ (equiv_extension_along_pforall@{v w u} Y)).
rapply (istrunc_extension_along_conn (n:=m) _ Y (HP:=istY)).
(** 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).
(** 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).
srapply (contr_equiv' ([O X, _] ->* Y)).
(** Every pointed type is (-1)-connected. *)
Global Instance is_minus_one_connected_pointed (X : pType)
: IsConnected (Tr (-1)) X
:= contr_inhabited_hprop _ (tr pt).