Merge pull request #746 from mikeshulman/lex-fibers

If a reflective subuniverse preserves fibers, it is a modality (and lex)

theories/Fibrations.v

@@ -65,9 +65,41 @@ Definition functor_hfiber {A B C D}
            (p : k o f == g o h) (b : B)
 : hfiber f b -> hfiber g (k b).
 Proof.
-  intros [a e].
-  exists (h a).
-  exact ((p a)^ @ ap k e).
+  rapply @functor_sigma.
+  - exact h.
+  - intros a e; exact ((p a)^ @ ap k e).
+Defined.
+
+(** ** The 3x3 lemma *)
+
+Definition hfiber_functor_hfiber {A B C D}
+           {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
+           (p : k o f == g o h) (b : B) (c : C) (q : g c = k b)
+: hfiber (functor_hfiber p b) (c;q)
+  <~> hfiber (functor_hfiber (fun x => (p x)^) c) (b;q^).
+Proof.
+  unfold hfiber, functor_hfiber, functor_sigma.
+  refine (_ oE (equiv_sigma_assoc _ _)^-1).
+  refine (equiv_sigma_assoc _ _ oE _).
+  apply (equiv_functor_sigma' 1); intros a; cbn.  
+  refine (_ oE
+         (equiv_functor_sigma'
+            (P := fun r => { s : h a = c & s # ((p a)^ @ ap k r) = q })
+            1 (fun r => equiv_path_sigma _
+                          (h a; (p a)^ @ ap k r) (c; q)))^-1).
+  refine (equiv_functor_sigma'
+            (P := fun r => { s : f a = b & s # (((p a)^)^ @ ap g r) = q^ })
+            1 (fun r => equiv_path_sigma _
+                          (f a; ((p a)^)^ @ ap g r) (b; q^)) oE _).
+  refine (equiv_sigma_symm _ oE _).
+  refine (equiv_functor_sigma' 1 _); intros r.
+  refine (equiv_functor_sigma' 1 _); intros s; cbn.
+  refine (equiv_concat_l (transport_paths_Fl _ _) _ oE _).
+  refine (_ oE (equiv_concat_l (transport_paths_Fl _ _) _)^-1).
+  refine ((equiv_ap inverse _ _)^-1 oE _).
+  refine (equiv_concat_r (inv_V q)^ _ oE _).
+  apply equiv_concat_l.
+  abstract (rewrite !inv_pp, !inv_V, concat_pp_p; reflexivity).
 Defined.
 
 (** ** Replacing a map with a fibration *)

theories/Modalities/Lex.v

@@ -1,6 +1,6 @@
 (* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
-Require Import Fibrations Extensions Pullback NullHomotopy.
+Require Import EquivalenceVarieties Fibrations Extensions Pullback NullHomotopy.
 Require Import Modality Accessible.
 Require Import HoTT.Tactics.
 
@@ -9,6 +9,8 @@ Local Open Scope path_scope.
 
 (** * Lex modalities *)
 
+(** ** Basic theory *)
+
 (** A lex modality is one that preserves finite limits, or equivalently pullbacks.  It turns out that a more basic and useful way to say this is that all path-spaces of connected types are connected.  Note how different this is from the behavior of, say, truncation modalities!
 
   This is a "large" definition, and we don't know of any small one that's equivalent to it (see <http://mathoverflow.net/questions/185980/a-small-definition-of-sub-%E2%88%9E-1-topoi>.  However, so far we never need to apply it "at multiple universes at once".  Thus, rather than making it a module type, we can make it a typeclass and rely on ordinary universe polymorphism. *)
@@ -24,7 +26,7 @@ Module Lex_Modalities_Theory (Os : Modalities).
 
   Global Existing Instance isconnected_paths.
 
-  (** The next six lemmas are equivalent characterizations of lex-ness. *)
+  (** The following numbered lemmas are all actually equivalent characterizations of lex-ness. *)
 
   (** 1. Every map between connected types is a connected map. *)
   Global Instance conn_map_lex {O : Modality} `{Lex O}
@@ -54,7 +56,7 @@ Module Lex_Modalities_Theory (Os : Modalities).
     (** Typeclass magic! *)
   Defined.
 
-  (** 4. Connected types are closed under pullbacks. *)
+  (** 4. Connected types are closed under pullbacks.  (Closure under fibers is [conn_map_lex] above. *)
   Global Instance isconnected_pullback (O : Modality) `{Lex O}
          {A B C : Type} {f : A -> C} {g : B -> C}
          `{IsConnected O A} `{IsConnected O B} `{IsConnected O C}
@@ -105,7 +107,35 @@ Module Lex_Modalities_Theory (Os : Modalities).
                 (hfiber_functor_pullback _ _ _ _ _ _ _ _ _ _)^-1 _).
   Qed.
 
-  (** 6. Lex modalities preserve path-spaces. *)
+  (** 6. The reflector preserves fibers.  This is a slightly simpler version of the previous. *)
+  Global Instance isequiv_O_functor_hfiber (O : Modality) `{Lex O}
+             {A B} (f : A -> B) (b : B)
+  : IsEquiv (O_functor_hfiber O f b).
+  Proof.
+    refine (isequiv_O_inverts O _).
+    apply O_inverts_conn_map.
+    refine (cancelR_conn_map O (to O _) _).
+    unfold O_functor_hfiber.
+    refine (conn_map_homotopic O
+             (@functor_hfiber _ _ _ _ f (O_functor O f) 
+                               (to O A) (to O B)
+                               (fun x => (to_O_natural O f x)^) b)
+             _ _ _).
+    - intros [a p].
+      rewrite O_rec_beta.
+      unfold functor_hfiber, functor_sigma. apply ap.
+      apply whiskerR, inv_V.
+    - intros [oa p].
+      refine (isconnected_equiv O _
+               (hfiber_functor_hfiber _ _ _ _)^-1 _).
+  Defined.
+
+  Definition equiv_O_functor_hfiber (O : Modality) `{Lex O}
+             {A B} (f : A -> B) (b : B)
+  : O (hfiber f b) <~> hfiber (O_functor O f) (to O B b)
+    := BuildEquiv _ _ (O_functor_hfiber O f b) _.
+
+  (** 7. Lex modalities preserve path-spaces. *)
   Definition O_path_cmp (O : Modality) {A} (x y : A)
   : O (x = y) -> (to O A x = to O A y)
     := O_rec (ap (to O A)).
@@ -151,6 +181,79 @@ Module Lex_Modalities_Theory (Os : Modalities).
 
 End Lex_Modalities_Theory.
 
+(** ** Lex reflective subuniverses *)
+
+(** A reflective subuniverse that preserves fibers is in fact a modality (and hence lex). *)
+Module Type Preserves_Fibers (Os : ReflectiveSubuniverses).
+
+  Export Os.
+  Module Export Os_Theory := ReflectiveSubuniverses_Theory Os.
+
+  Parameter isequiv_O_functor_hfiber :
+     forall (O : ReflectiveSubuniverse) {A B} (f : A -> B) (b : B),
+       IsEquiv (O_functor_hfiber O f b).
+
+End Preserves_Fibers.
+
+(** We omit the module type as with [ReflectiveSubuniverses_to_Modalities]; see below. *)
+Module Lex_Reflective_Subuniverses
+       (Os : ReflectiveSubuniverses) (Opf : Preserves_Fibers Os).
+  (** <: SigmaClosed Os. *)
+
+  Import Opf.
+
+  Definition inO_sigma (O : ReflectiveSubuniverse@{u a})
+             (A:Type@{i}) (B:A -> Type@{j})
+             (A_inO : In@{u a i} O A)
+             (B_inO : forall a, In@{u a j} O (B a))
+  : In@{u a k} O {x:A & B x}.
+  Proof.
+    pose (g := O_rec pr1 : O {x : A & B x} -> A).
+    transparent assert (p : (forall x, g (to O _ x) = x.1)).
+    { intros x; subst g; apply O_rec_beta. }
+    apply inO_isequiv_to_O.
+    apply isequiv_fcontr; intros x.
+    refine (contr_equiv' _ (hfiber_hfiber_compose_map _ g x)).
+    apply fcontr_isequiv.
+    unfold hfiber_compose_map.
+    transparent assert (h : (hfiber (@pr1 A B) (g x) <~> hfiber g (g x))).
+    { refine (_ oE equiv_to_O O _).
+      - refine (_ oE BuildEquiv _ _ (O_functor_hfiber O (@pr1 A B) (g x)) _).
+        unfold hfiber.
+        refine (equiv_functor_sigma' 1 _). intros y; cbn.
+        refine (_ oE (equiv_moveR_equiv_V _ _)).
+        apply equiv_concat_l.
+        apply moveL_equiv_V.
+        unfold g, O_functor.
+        revert y; apply O_indpaths; intros [a q]; cbn.
+        refine (_ @ (O_rec_beta _ _)^).
+        apply ap, O_rec_beta.
+      - refine (inO_equiv_inO _ (hfiber_fibration (g x) B)). }
+    refine (isequiv_homotopic (h oE equiv_hfiber_homotopic _ _ p (g x)) _).
+    intros [[a b] q]; cbn. clear h.
+    unfold O_functor_hfiber.
+    rewrite O_rec_beta.
+    unfold functor_sigma; cbn.
+    refine (path_sigma' _ 1 _).
+    rewrite O_indpaths_beta; cbn.
+    unfold moveL_equiv_V, moveR_equiv_V.
+    Open Scope long_path_scope.
+    rewrite !ap_pp, !concat_p_pp, !ap_V.
+    unfold to_O_natural.
+    rewrite concat_pV_p.
+    subst p.
+    rewrite concat_pp_V.
+    rewrite concat_pp_p; apply moveR_Vp.
+    rewrite <- !(ap_compose (to O A) (to O A)^-1).
+    rapply @concat_A1p.
+    Close Scope long_path_scope.
+  Qed.
+
+(** As with [ReflectiveSubuniverses_to_Modalities], Coq won't actually accept this as a module of type [SigmaClosed Os] because the above proof introduces way too many universe parameters.  It might be possible to bring it down to become acceptable with heavy use of universe annotations, but this is probably not worthwhile bothering about because the only point of [SigmaClosed] is to be passed to [ReflectiveSubuniverses_to_Modalities], which in turn can't actually instantiate [Modalities] for more fundamental reasons.  *)
+End Lex_Reflective_Subuniverses.
+
+(** ** Accessible lex modalities *)
+
 (** We now restrict to lex modalities that are also accessible. *)
 Module Accessible_Lex_Modalities_Theory
        (Os : Modalities)

theories/Modalities/ReflectiveSubuniverse.v

@@ -806,6 +806,16 @@ Section Reflective_Subuniverse.
 
     Hint Immediate inO_unsigma : typeclass_instances.
 
+    (** The reflector preserving hfibers is a characterization of lex modalities.  Here is the comparison map. *)
+    Definition O_functor_hfiber {A B} (f : A -> B) (b : B)
+    : O (hfiber f b) -> hfiber (O_functor f) (to O B b).
+    Proof.
+      apply O_rec. intros [a p].
+      exists (to O A a).
+      refine (to_O_natural f a @ _).
+      apply ap, p.
+    Defined.
+
     (** ** Paths *)
 
     Global Instance inO_paths (S : Type) {S_inO : In O S} (x y : S)