Merge pull request #2371 from jdchristensen/isconnmap_connected

Modalities: generalize OO_conn_map_isconnected and other results

Author: jdchristensen

theories/Modalities/Descent.v

@@ -215,7 +215,7 @@ Definition equiv_path_OO `{O' <= Sep O}
   : O (x = y) <~> (to O' X x = to O' X y)
   := Build_Equiv _ _ (path_OO x y) _.
 
-(** [functor_hfiber] on a pair of [O']-equivalences is an [O]-equivalence. *)
+(** [functor_hfiber] on a pair of [O']-equivalences is an [O]-equivalence. Is this true when [h] is only assumed to be an [O]-equivalence? (See strengthened version of [OO_conn_map_isconnected] below.) *)
 #[export] Instance OO_inverts_functor_hfiber
        {A B C D : Type} {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
        (p : k o f == g o h) (b : B)
@@ -244,33 +244,41 @@ Definition equiv_OO_functor_hfiber_to_O
   : O (hfiber f x) <~> O (hfiber (O_functor O' f) (to O' X x))
   := Build_Equiv _ _ _ (OO_inverts_functor_hfiber_to_O f x).
 
-(** Theorem 3.1(iii) of RSS: any map between [O']-connected types is [O]-connected.  (Part (ii) is just the version for dependent projections.) *)
+(** Any map from an [O]-connected type to an [O']-connected type is [O]-connected.  Taking [O = O'] gives Theorem 3.1(iii) of RSS. (Part (ii) is just the version for dependent projections.) *)
 Definition OO_conn_map_isconnected
-       {Y X : Type} `{IsConnected O' Y, IsConnected O' X} (f : Y -> X)
+       {Y X : Type} `{IsConnected O Y, IsConnected O' X} (f : Y -> X)
   : IsConnMap O f.
 Proof.
-  intros x; exact (contr_equiv' _ (equiv_OO_functor_hfiber_to_O f x)^-1).
+  intros x; unfold IsConnected.
+  rapply (contr_equiv' (O Y)).
+  (* By the previous result, [O] of the fiber is equivalent to [O] of the fiber of [O_functor O' f]: *)
+  rhs' napply (equiv_OO_functor_hfiber_to_O f x).
+  (* And [O Y] is equivalent to [O (O' Y)]: *)
+  lhs' rapply (equiv_O_functor_to_O_O_leq O O' Y).
+  (* Finally, since [O' X] is contractible, the fiber is the same as the domain [O' Y]. *)
+  apply equiv_O_functor.
+  symmetry; rapply equiv_sigma_contr.
 Defined.
 
 Definition OO_isconnected_hfiber
-       {Y X : Type} `{IsConnected O' Y, IsConnected O' X} (f : Y -> X) (x : X)
+       {Y X : Type} `{IsConnected O Y, IsConnected O' X} (f : Y -> X) (x : X)
   : IsConnected O (hfiber f x)
   := OO_conn_map_isconnected f x.
 
-(** Theorem 3.1(iv) of RSS: an [O]-modal map between [O']-connected types is an equivalence. *)
+(** An [O]-modal map from an [O]-connected type to an [O']-connected type is an equivalence.  When [O = O'], this gives Theorem 3.1(iv) of RSS. *)
 Definition OO_isequiv_mapino_isconnected
-       {Y X : Type} `{IsConnected O' Y, IsConnected O' X} (f : Y -> X) `{MapIn O _ _ f}
+       {Y X : Type} `{IsConnected O Y, IsConnected O' X} (f : Y -> X) `{MapIn O _ _ f}
   : IsEquiv f.
 Proof.
   apply (isequiv_conn_ino_map O).
   - apply OO_conn_map_isconnected.
   - assumption.
 Defined.
 
-(** Theorem 3.1(vi) of RSS (and part (v) is just the analogue for dependent projections). *)
+(** When [O = O'], this is Theorem 3.1(vi) of RSS.  (Part (v) is just the analogue for dependent projections.) *)
 Definition OO_conn_map_functor_hfiber {A B C D : Type}
            {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
-           `{IsConnMap O' _ _ h, IsConnMap O' _ _ k}
+           `{IsConnMap O _ _ h, IsConnMap O' _ _ k}
            (p : k o f == g o h) (b : B)
   : IsConnMap O (functor_hfiber p b).
 Proof.

theories/Modalities/ReflectiveSubuniverse.v

@@ -2038,6 +2038,12 @@ Proof.
   apply (ooextendable_O_inverts O2); exact _.
 Defined.
 
+(** In particular, we get that [O1 A] is equivalent to [O1 (O2 A)]. *)
+Definition equiv_O_functor_to_O_O_leq@{i1 i2}
+           (O1 : ReflectiveSubuniverse@{i1}) (O2 : ReflectiveSubuniverse@{i2}) `{O_leq@{i1 i2 i1} O1 O2}
+           (A : Type@{i1})
+  : O1 A <~> O1 (O2 A)
+  := Build_Equiv _ _ _ (O_inverts_O_leq O1 O2 (to O2 A)).
 
 (** ** Equality of (reflective) subuniverses *)
 

theories/Truncations/Connectedness.v

@@ -29,6 +29,14 @@ A handy benchmark: under our indexing, the map [S1 -> 1] is 0-connected but not
 
 One reason for our choice is that this way, the n-truncated and n-connected maps are the modal and modally-connected maps for the n-truncation modality.  Many of the basic lemmas about connected maps are in fact true for any modality, and can be found in [Modality.v].  Thus, here we consider mainly properties that involve the interaction of connectedness at different truncation levels. *)
 
+(** ** Connectedness of maps between connected types *)
+
+(** If [X] is n-connected and [Y] is (n+1)-connected, then any map [X -> Y] is n-connected. *)
+Definition isconnmap_isconnected `{Univalence} (n : trunc_index)
+  (X Y : Type) `{IsConnected n X} `{IsConnected n.+1 Y} (f : X -> Y)
+  : IsConnMap n f
+  := OO_conn_map_isconnected (Tr n.+1) (Tr n) f.
+
 (** ** Truncatedness of the type of extensions *)
 
 (** A key lemma on the interaction between connectedness and truncatedness: suppose one is trying to extend along an n-connected map, into a k-truncated family of types (k ≥ n).  Then the space of possible extensions is (k–n–2)-truncated.
@@ -108,11 +116,8 @@ Defined.
 
 Definition conn_point_incl `{Univalence} {n : trunc_index} {A : Type} (a0:A)
   `{IsConnected n.+1 A}
-  : IsConnMap n (unit_name a0).
-Proof.
-  rapply (OO_cancelL_conn_map (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)).
-  apply O_lex_leq_Tr.
-Defined.
+  : IsConnMap n (unit_name a0)
+  := OO_cancelL_conn_map (Tr n.+1) (Tr n) (unit_name a0) (const_tt A).
 
 (** [conn_point_incl] can be made an instance, but at the time of writing, this doesn't cause any additional goals to be solved compared to making it an immediate hint, so we do the latter. *)
 #[export] Hint Immediate conn_point_incl : typeclass_instances.

theories/Truncations/SeparatedTrunc.v

@@ -30,8 +30,7 @@ Proof.
   srapply O_strong_leq_trans_l.
 Defined.
 
-(** For some reason, this causes typeclass search to spin. *)
-Local Instance O_lex_leq_Tr `{Univalence} (n : trunc_index)
+#[export] Instance O_lex_leq_Tr `{Univalence} (n : trunc_index)
   : Tr n <<< Tr n.+1.
 Proof.
   intros A; unshelve econstructor; intros P' P_inO;