Truncatedness of pointed maps and pForall

theories/Homotopy/ClassifyingSpace.v

@@ -575,7 +575,7 @@ Proof.
     refine (natequiv_opyon_equiv _^-1$).
     rapply pequiv_pclassifyingspace_pi1. }
   snrapply Build_NatEquiv.
-  1: intro; exact equiv_ptr_rec.
+  1: intro; exact pequiv_ptr_rec.
   rapply is1natural_prewhisker.
 Defined.
 

theories/Modalities/Modality.v

@@ -160,6 +160,15 @@ Proof.
   rapply Build_Modality'.
 Defined.
 
+(** When combined with [isequiv_oD_to_O], this yields Theorem 7.7.7 in the book. *)
+Definition isequiv_oD_to_O_modality
+           `{Funext} (O : Modality) {A : Type}
+           (B : O A -> Type) `{forall a, In O (B a)}
+  : IsEquiv (fun (h : forall oa, B oa) => h oD to O A).
+Proof.
+  srapply (isequiv_oD_to_O O O).
+Defined.
+
 (** Of course, modalities have dependent eliminators. *)
 Definition O_ind {O : Subuniverse} {A : Type} `{ReflectsD O O A}
   := @OO_ind O O A _ _.
@@ -199,15 +208,6 @@ Proof.
     + rapply inO_paths'.
 Defined.
 
-(** When combined with [isequiv_oD_to_O], this yields Theorem 7.7.7 in the book. *)
-Definition isequiv_oD_to_O_modality
-           `{Funext} (O : Modality) {A : Type}
-           (B : O A -> Type) `{forall a, In O (B a)}
-  : IsEquiv (fun (h : forall oa, B oa) => h oD to O A).
-Proof.
-  srapply (isequiv_oD_to_O O O).
-Defined.
-
 (** A tactic that extends [strip_reflections] to modalities. It handles non-dependent elimination for reflective subuniverses and dependent elimination for modalities. [strip_truncations] does the same for truncations, but introduces fewer universe variables, so tends to work better when removing truncations. *)
 Ltac strip_modalities :=
   (** Search for hypotheses of type [O X] for some [O] such that the goal is [O]-local. *)

theories/Modalities/ReflectiveSubuniverse.v

@@ -1452,6 +1452,10 @@ Section ConnectedTypes.
                                     (ooextendable_const_isconnected_inO A C))).
   Defined.
 
+  Definition equiv_const_isconnected_inO `{Funext}
+             {A : Type} `{IsConnected O A} (C : Type) `{In O C}
+  : C <~> (A -> C) := Build_Equiv _ _ const (isequiv_const_isconnected_inO C).
+
 End ConnectedTypes.
 
 (** ** Modally truncated maps *)

theories/Pointed/Core.v

@@ -4,6 +4,7 @@ Require Import PathAny.
 Require Import WildCat.
 Require Import Truncations.Core.
 Require Import ReflectiveSubuniverse.
+Require Import Extensions.
 
 Local Set Polymorphic Inductive Cumulativity.
 
@@ -71,6 +72,9 @@ Definition Build_pMap (A B : pType) (f : A -> B) (p : f (point A) = point B)
   : A ->* B
   := Build_pForall A (pfam_const B) f p.
 
+(** The [&] tells Coq to use the context to infer the later arguments (in this case, all of them). *)
+Arguments Build_pMap & _ _ _ _.
+
 (** Pointed maps perserve the base point *)
 Definition point_eq {A B : pType} (f : A ->* B)
   : f (point A) = point B
@@ -235,6 +239,16 @@ Definition issig_pequiv' (A B : pType)
   : {f : A <~> B & f (point A) = point B} <~> (A <~>* B)
   := ltac:(make_equiv).
 
+(** pForall can also be described as a type of extensions. *)
+Definition equiv_extension_along_pforall `{Funext} {A : pType} (P : pFam A)
+  : ExtensionAlong (unit_name (point A)) P (unit_name (dpoint P)) <~> pForall A P.
+Proof.
+  unfold ExtensionAlong.
+  refine (issig_pforall A P oE _).
+  apply equiv_functor_sigma_id; intro s.
+  symmetry; apply equiv_unit_rec.
+Defined.
+
 (** This is [equiv_prod_coind] for pointed families. *)
 Definition equiv_pprod_coind {A : pType} (P Q : pFam A)
   : (pForall A P * pForall A Q) <~>
@@ -429,14 +443,10 @@ Definition pointed_fam {A : pType} (B : A -> pType) : pFam A
 Definition point_pforall {A : pType} (B : A -> pType) : pForall A (pointed_fam B)
   := Build_pForall A (pointed_fam B) (fun x => point (B x)) 1.
 
-(** The pointed type of pointed maps. For dependent pointed maps we need a family of pointed types, not just a family of types with a point over the basepoint of [A]. *)
+(** The pointed type of dependent pointed maps. Note that we need a family of pointed types, not just a family of types with a point over the basepoint of [A]. *)
 Definition ppForall (A : pType) (B : A -> pType) : pType
   := [pForall A (pointed_fam B), point_pforall B].
 
-Definition ppMap (A B : pType) : pType
-  := ppForall A (fun _ => B).
-
-Infix "->**" := ppMap : pointed_scope.
 Notation "'ppforall'  x .. y , P"
   := (ppForall _ (fun x => .. (ppForall _ (fun y => P)) ..))
      : pointed_scope.
@@ -445,6 +455,12 @@ Notation "'ppforall'  x .. y , P"
 Definition pconst {A B : pType} : A ->* B
   := point_pforall (fun _ => B).
 
+(** The pointed type of pointed maps.  This is a special case of [ppForall]. *)
+Definition ppMap (A B : pType) : pType
+  := [A ->* B, pconst].
+
+Infix "->**" := ppMap : pointed_scope.
+
 Lemma pmap_punit_pconst {A : pType} (f : A ->* pUnit) : pconst ==* f.
 Proof.
   srapply Build_pHomotopy.
@@ -459,6 +475,14 @@ Proof.
   exact (concat_1p _)^.
 Defined.
 
+Global Instance contr_pmap_from_contr `{Funext} {A B : pType} `{C : Contr A}
+  : Contr (A ->* B).
+Proof.
+  rapply (contr_equiv' { b : B & b = pt }).
+  refine (issig_pmap A B oE _).
+  exact (equiv_functor_sigma_pb (equiv_arrow_from_contr A B)^-1%equiv).
+Defined.
+
 (** * pType and pForall as wild categories *)
 
 (** Note that the definitions for [pForall] are also used for the higher structure in [pType]. *)

theories/Pointed/pModality.v

@@ -1,8 +1,10 @@
-Require Import Basics Types ReflectiveSubuniverse Pointed.Core.
+Require Import Basics Types ReflectiveSubuniverse Pointed.Core Pointed.pEquiv.
 
 Local Open Scope pointed_scope.
 
-(** * Modalities and pointed types *)
+(** * Modalities, reflective subuniverses and pointed types *)
+
+(** So far, everything is about general reflective subuniverses, but in the future results about modalities can be placed here as well. *)
 
 Global Instance ispointed_O `{O : ReflectiveSubuniverse} (X : Type)
   `{IsPointed X} : IsPointed (O X) := to O _ (point X).
@@ -31,6 +33,25 @@ Proof.
   exact (concat_1p _)^.
 Defined.
 
+(** A pointed version of the universal property. *)
+Definition pequiv_o_pto_O `{Funext}
+  (O : ReflectiveSubuniverse) (P Q : pType) `{In O Q}
+  : ([O P, _] ->** Q) <~>* (P ->** Q).
+Proof.
+  snrapply Build_pEquiv.
+  (* We could just use the map [e] defined in the next bullet, but we want Coq to immediately unfold the underlying map to this. *)
+  - exact (Build_pMap _ _ (fun f => f o* pto O P) 1).
+  (* We'll give an equivalence that definitionally has the same underlying map. *)
+  - transparent assert (e : (([O P, _] ->* Q) <~> (P ->* Q))).
+    + refine (issig_pmap P Q oE _ oE (issig_pmap [O P, _] Q)^-1%equiv).
+      snrapply equiv_functor_sigma'.
+      * rapply equiv_o_to_O.
+      * intro f; cbn.
+      (* [reflexivity] works here, but then the underlying map won't agree definitionally with precomposition by [pto P], since pointed composition inserts a reflexivity path here. *)
+      apply (equiv_concat_l 1).
+    + apply (equiv_isequiv e).
+Defined.
+
 (** ** Pointed functoriality *)
 
 Definition O_pfunctor `(O : ReflectiveSubuniverse) {X Y : pType}

theories/Pointed/pTrunc.v

@@ -1,10 +1,12 @@
-Require Import Basics Types WildCat Truncations.Core Truncations.SeparatedTrunc
+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, _].
 
@@ -42,21 +44,9 @@ Definition pTr_ind n {X : pType} {Y : pFam (pTr n X)} `{forall x, IsTrunc n (Y x
   : pForall (pTr n X) Y
   := Build_pForall (pTr n X) Y (Trunc_ind Y f) (dpoint_eq f).
 
-Definition equiv_ptr_rec `{Funext} {n} {X Y : pType} `{IsTrunc n Y}
-  : (pTr n X ->* Y) <~> (X ->* Y).
-Proof.
-  srapply equiv_adjointify.
-  { intro f.
-    exact (f o* ptr). }
-  1: srapply pTr_rec.
-  1: nrapply pTr_rec_beta_path.
-  intro f.
-  apply path_pforall.
-  srapply Build_pHomotopy.
-  1: by rapply Trunc_ind.
-  cbn.
-  symmetry; apply concat_pp_V.
-Defined.
+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] *)
 
@@ -104,7 +94,7 @@ Proof.
   reflexivity.
 Defined.
 
-Definition ptr_pequiv {X Y : pType} (n : trunc_index) (f : X <~>* Y)
+Definition pequiv_ptr_functor {X Y : pType} (n : trunc_index) (f : X <~>* Y)
   : pTr n X <~>* pTr n Y
   := emap (pTr n) f.
 
@@ -135,21 +125,11 @@ 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).
 
-Definition pequiv_ptr_functor {X Y : pType} n
-  : X <~>* Y -> pTr n X <~>* pTr n Y.
-Proof.
-  intro e.
-  srapply Build_pEquiv.
-  1: rapply (fmap (pTr _) e).
-  exact _.
-Defined.
-
 (* 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)
-  : (@path_Tr n A a0 a1) o tr == ap tr.
+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.
-  intro p; induction p.
-  reflexivity.
+  by destruct p.
 Defined.
 
 (* [ptr_loops] commutes with the two [ptr] maps. *)
@@ -168,3 +148,29 @@ Proof.
     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. *)
+Definition istrunc_pforall `{Univalence} {m n : trunc_index}
+  (X : pType) {iscX : IsConnected m.+1 X}
+  (Y : pFam X) {istY : forall x, IsTrunc (n +2+ m) (Y x)}
+  : IsTrunc n (pForall X Y).
+Proof.
+  nrapply (istrunc_equiv_istrunc _ (equiv_extension_along_pforall 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).
+
+(** 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 provied 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.

theories/Spectra/Spectrum.v

@@ -37,7 +37,7 @@ Definition strunc `{Univalence} (k : trunc_index) (E : Spectrum) : Spectrum.
 Proof.
   simple refine (Build_Spectrum (Build_Prespectrum (fun n => pTr (trunc_index_inc k n) (E n)) _) _).
   - intros n.
-    exact ((ptr_loops _ (E n.+1)) o*E (ptr_pequiv _ (equiv_glue E n))).
+    exact ((ptr_loops _ (E n.+1)) o*E (pequiv_ptr_functor _ (equiv_glue E n))).
   - intros n. unfold glue.
     srapply isequiv_compose.
 Defined.

theories/Truncations/Connectedness.v

@@ -95,7 +95,7 @@ Proof.
   (** This follows from [conn_point_incl] and [conn_map_elim], but we give a direct proof. *)
   intro a.
   (** Since [A] is [n+1]-connected, [a0 = a] is [n]-connected, which means that [Tr n (a0 = a)] has an element. *)
-  pose proof (p := center _ : Tr n ((point A) = a)).
+  pose proof (p := center (Tr n ((point A) = a))).
   strip_truncations.
   exact (p # p0).
 Defined.

theories/Truncations/Core.v

@@ -297,7 +297,7 @@ Ltac strip_truncations :=
 
 (** ** Iterated truncations *)
 
-(** Compare to [O_leq_Tr] below. *)
+(** Compare to [O_leq_Tr] and [O_strong_leq_Tr] in SeparatedTrunc.v. *)
 Definition O_leq_Tr_leq {n m : trunc_index} (Hmn : m <= n)
   : O_leq (Tr m) (Tr n).
 Proof.

theories/Truncations/SeparatedTrunc.v

@@ -43,7 +43,7 @@ Proof.
   - intros; cbn. reflexivity.
 Defined.
 
-Definition path_Tr {n A} (x y : A)
+Definition path_Tr {n A} {x y : A}
   : Tr n (x = y) -> (tr x = tr y :> Tr n.+1 A)
   := path_OO (Tr n.+1) (Tr n) x y.
 

theories/Types/Arrow.v

@@ -2,7 +2,7 @@
 (** * Theorems about Non-dependent function types *)
 
 Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable
-               Basics.Equivalences Basics.Trunc.
+               Basics.Equivalences Basics.Trunc Basics.Tactics.
 Require Import Types.Forall.
 Local Open Scope path_scope.
 
@@ -209,6 +209,18 @@ Global Instance istrunc_arrow {A B : Type} `{IsTrunc n B}
   : IsTrunc n (A -> B) | 100
   := istrunc_forall.
 
+(** ** Functions from a contractible type *)
+
+(** This also follows from [equiv_contr_forall], but this proof has a better inverse map. *)
+Definition equiv_arrow_from_contr (A B : Type) `{Contr A}
+  : (A -> B) <~> B.
+Proof.
+  srapply (equiv_adjointify (fun f => f (center A)) const).
+  - reflexivity.
+  - intro f; funext a; unfold const; simpl.
+    apply (ap f), contr.
+Defined.
+
 (** ** Equivalences *)
 
 Global Instance isequiv_functor_arrow `{IsEquiv B A f} `{IsEquiv C D g}