Merge pull request #1408 from mikeshulman/lexloc

Lex localizations (ABFJ)

theories/Modalities/Descent.v

@@ -133,22 +133,12 @@ Definition ooextendable_TypeO_lex_leq `{Univalence}
            {A B : Type} (f : A -> B) `{O_inverts O' f}
   : ooExtendableAlong f (fun _ => Type_ O).
 Proof.
-  (** It suffices to show that maps into [Type_ O] extend along [f], and that sections of families of equivalences are [ooExtendableAlong] it.  However, due to the implementation of [ooExtendableAlong], we have to prove the first one twice (there should probably be a general cofixpoint lemma for this). *)
-  intros [|[|n]];
-    [ exact tt
-    | split; [ intros P | intros; exact tt ]
-    | split; [ intros P | ] ].
-  (** The first follows from what we just proved. *)
-  1-2:exists (fun x => (OO_descend_O_inverts f P x ;
-                        OO_descend_O_inverts_inO f P x)).
-  1-2:intros x; apply path_TypeO, path_universe_uncurried; cbn. 
-  1-2:exact (OO_descend_O_inverts_beta f P x).
-  (** The second follows from the fact that the type of equivalences between two [O]-modal types is [O]-modal. *)
-  intros P Q; rapply (ooextendable_postcompose' (fun b => P b <~> Q b)).
-  - intros x; refine (equiv_path_TypeO _ _ _ oE equiv_path_universe _ _).
-  - (** Typeclass inference spins on [rapply], I don't know why. *)
-    apply (ooextendable_conn_map_inO O); exact _.
-Defined.  
+  rapply ooextendable_TypeO_from_extension; intros P.
+  exists (fun x => (OO_descend_O_inverts f P x ;
+                    OO_descend_O_inverts_inO f P x)).
+  intros x; apply path_TypeO, path_universe_uncurried; cbn.
+  exact (OO_descend_O_inverts_beta f P x).
+Defined.
 
 (** We can also state it in terms of belonging to a subuniverse if we lift [O'] accessibly (an analogue of Theorem 3.11(iii) of RSS). *)
 Global Instance inO_TypeO_lex_leq `{Univalence} `{IsAccRSU O'}

theories/Modalities/Lex.v

@@ -364,3 +364,26 @@ Proof.
   Local Transparent eissect. (* work around bug 4533 *)
   Close Scope long_path_scope.
 Qed.
+
+(** ** Lexness via generators *)
+
+(** Here the characterization of when an accessible presentation yields a lex modality from Anel-Biederman-Finster-Joyal ("Higher Sheaves and Left-Exact Localizations of ∞-Topoi", arXiv:2101.02791): it's enough for path spaces of the generators to be connected. *)
+Definition lex_gen `{Univalence} (O : Modality) `{IsAccModality O}
+           (lexgen : forall (i : ngen_indices (acc_ngen O)) (x y : ngen_type (acc_ngen O) i),
+               IsConnected O (x = y))
+  : Lex O.
+Proof.
+  srapply lex_from_inO_typeO; [ exact _ | intros i ].
+  rapply ooextendable_TypeO_from_extension; intros P; srefine (_;_).
+  1:intros; exists (forall x, P x); exact _.
+  assert (wc : forall y z, P y <~> P z).
+  { intros y z.
+    (** Here we use the hypothesis [lexgen] (typeclass inference finds it automatically). *)
+    refine (pr1 (isconnected_elim O _ (equiv_transport P y z))). }
+  intros x; apply path_TypeO, path_universe_uncurried.
+  refine (equiv_adjointify (fun f => f x) (fun u y => wc x y ((wc x x)^-1 u)) _ _).
+  - intros u; apply eisretr.
+  - intros f; apply path_forall; intros y; apply moveR_equiv_M.
+    destruct (isconnected_elim O _ (fun y => (wc x y)^-1 (f y))) as [z p].
+    exact (p x @ (p y)^).
+Defined.

theories/Modalities/ReflectiveSubuniverse.v

@@ -1628,6 +1628,24 @@ Section ConnectedMaps.
   : (forall b, P b) <~> (forall a, P (f a))
   := Build_Equiv _ _ _ (isequiv_o_conn_map f P).
 
+  (** When considering lexness properties, we often want to consider the property of the universe of modal types being modal.  We can't say this directly (except in the accessible, hence liftable, case) because it lives in a higher universe, but we can make a direct extendability statement.  Here we prove a lemma that oo-extendability into the universe follows from plain extendability, essentially because the type of equivalences between two [O]-modal types is [O]-modal. *)
+  Definition ooextendable_TypeO_from_extension
+             {A B : Type} (f : A -> B) `{IsConnMap O _ _ f}
+             (extP : forall P : A -> Type_ O, ExtensionAlong f (fun _ : B => Type_ O) P)
+    : ooExtendableAlong f (fun _ => Type_ O).
+  Proof.
+    (** By definition, in addition to our assumption [extP] that maps into [Type_ O] extend along [f], we must show that sections of families of equivalences are [ooExtendableAlong] it.  *)
+    intros [|[|n]].
+    - exact tt.                                 (* n = 0 *)
+    (** Note that due to the implementation of [ooExtendableAlong], we actually have to use [extP] twice (there should probably be a general cofixpoint lemma for this). *)
+    - split; [ apply extP | intros; exact tt ]. (* n = 1 *)
+    - split; [ apply extP | ].                  (* n > 1 *)
+      (** What remains is to extend families of paths. *)
+      intros P Q; rapply (ooextendable_postcompose' (fun b => P b <~> Q b)).
+      + intros x; refine (equiv_path_TypeO _ _ _ oE equiv_path_universe _ _).
+      + rapply ooextendable_conn_map_inO.
+  Defined.
+
   (** Conversely, if a map satisfies this elimination principle (expressed via extensions), then it is connected.  This completes the proof of Lemma 7.5.7 from the book. *)
   Lemma conn_map_from_extension_elim {A B : Type} (f : A -> B)
   : (forall (P : B -> Type) {P_inO : forall b:B, In O (P b)}