From c7c1ea42b08cebaf9389cd7be5d94df18c148f56 Mon Sep 17 00:00:00 2001
From: Mike Shulman <shulman@sandiego.edu>
Date: Wed, 13 Jan 2021 14:36:34 -0800
Subject: [PATCH 1/5] split off extendable -> ooextendable for the universe

---
 theories/Modalities/Descent.v               | 22 ++++++---------------
 theories/Modalities/ReflectiveSubuniverse.v | 16 +++++++++++++++
 2 files changed, 22 insertions(+), 16 deletions(-)

diff --git a/theories/Modalities/Descent.v b/theories/Modalities/Descent.v
index 1657d6cbf34..6c76611d734 100644
--- a/theories/Modalities/Descent.v
+++ b/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'}
diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
index d794b4b61a3..e51301c17d0 100644
--- a/theories/Modalities/ReflectiveSubuniverse.v
+++ b/theories/Modalities/ReflectiveSubuniverse.v
@@ -1628,6 +1628,22 @@ 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.
+    (** 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; [ apply extP | intros; exact tt ]
+      | split; [ apply extP | ] ].
+    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)}

From 071364c2619e840f819460ecdf4ae1d6d1ce8745 Mon Sep 17 00:00:00 2001
From: Mike Shulman <shulman@sandiego.edu>
Date: Wed, 13 Jan 2021 14:36:47 -0800
Subject: [PATCH 2/5] Lexness via generators result from ABFJ

---
 theories/Modalities/Lex.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/theories/Modalities/Lex.v b/theories/Modalities/Lex.v
index eb61e07035d..ebb326d041d 100644
--- a/theories/Modalities/Lex.v
+++ b/theories/Modalities/Lex.v
@@ -364,3 +364,24 @@ 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; 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.

From 49f366e13143fdcd6d6083d678fca9b337c7edaf Mon Sep 17 00:00:00 2001
From: Mike Shulman <shulman@sandiego.edu>
Date: Thu, 14 Jan 2021 08:32:59 -0800
Subject: [PATCH 3/5] break out proof of ooextendable_TypeO_from_extension into
 bullets

---
 theories/Modalities/ReflectiveSubuniverse.v | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
index e51301c17d0..f03fbf9b0f4 100644
--- a/theories/Modalities/ReflectiveSubuniverse.v
+++ b/theories/Modalities/ReflectiveSubuniverse.v
@@ -1635,13 +1635,14 @@ Section ConnectedMaps.
     : 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; [ apply extP | intros; exact tt ]
-      | split; [ apply extP | ] ].
-    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.
+    intros [|[|n]].
+    - exact tt.                                 (* n = 0 *)
+    - split; [ apply extP | intros; exact tt ]. (* n = 1 *)
+    - split; [ apply extP | ].                  (* n > 1 *)
+      (** After applying the hypothesis [extP], 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. *)

From 0f5b47675a1ee59d6d5af4e68911654baddaddb1 Mon Sep 17 00:00:00 2001
From: Mike Shulman <shulman@sandiego.edu>
Date: Thu, 14 Jan 2021 08:35:18 -0800
Subject: [PATCH 4/5] comment on use of hypothesis in lex_gen

---
 theories/Modalities/Lex.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/Modalities/Lex.v b/theories/Modalities/Lex.v
index ebb326d041d..58c96d031c8 100644
--- a/theories/Modalities/Lex.v
+++ b/theories/Modalities/Lex.v
@@ -377,7 +377,9 @@ Proof.
   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; refine (pr1 (isconnected_elim O _ (equiv_transport P y 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.

From 3c8a78f2dee08d738f89e787606cc62e2565d61f Mon Sep 17 00:00:00 2001
From: Mike Shulman <shulman@sandiego.edu>
Date: Thu, 14 Jan 2021 10:28:41 -0800
Subject: [PATCH 5/5] improve comments in ooextendable_TypeO_from_extension

---
 theories/Modalities/ReflectiveSubuniverse.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
index f03fbf9b0f4..27243d03e5c 100644
--- a/theories/Modalities/ReflectiveSubuniverse.v
+++ b/theories/Modalities/ReflectiveSubuniverse.v
@@ -1634,12 +1634,13 @@ Section ConnectedMaps.
              (extP : forall P : A -> Type_ O, ExtensionAlong f (fun _ : B => Type_ O) P)
     : 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). *)
+    (** 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 *)
-      (** After applying the hypothesis [extP], what remains is to extend families of paths. *)
+      (** 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.