Require Import HoTT.Basics HoTT.Types HoTT.Cubical.DPath.Require Import HoTT.Basics HoTT.Types HoTT.Cubical.DPath.
Require Import HFiber Extensions Factorization Limits.Pullback.
Require Import Modality Accessible Descent.
Require Import Truncations.Core.
Require Import Homotopy.Suspension.

Local Open Scope path_scope.
Local Open Scope subuniverse_scope.

(** * Subuniverses of separated types *)

(** The basic reference for subuniverses of separated types is
  - Christensen, Opie, Rijke, and Scoccola, "Localization in Homotopy Type Theory", https://arxiv.org/abs/1807.04155.
hereinafter referred to as "CORS".  *)

(** ** Definition *)

(** The definition is in [ReflectiveSubuniverse.v]. *)

(** ** Basic properties *)

(** A function is (fiberwise) in [Sep O] exactly when its diagonal is in [O]. *)

Section Diagonal.
  Context (O : Subuniverse) {X Y : Type} (f : X -> Y).

  Definition mapinO_diagonal `{MapIn (Sep O) _ _ f} : MapIn O (diagonal f).
O: Subuniverse
X, Y: Type
f: X -> Y
H: MapIn (Sep O) f
MapIn O (diagonal f)
  Proof.
O: Subuniverse
X, Y: Type
f: X -> Y
H: MapIn (Sep O) f
MapIn O (diagonal f)
    intros p.
O: Subuniverse
X, Y: Type
f: X -> Y
H: MapIn (Sep O) f
p: Pullback f f
In O (hfiber (diagonal f) p)
    exact (inO_equiv_inO' _ (hfiber_diagonal f p)^-1).
  Defined.

  Definition mapinO_from_diagonal `{MapIn O _ _ (diagonal f)} : MapIn (Sep O) f.
O: Subuniverse
X, Y: Type
f: X -> Y
H: MapIn O (diagonal f)
MapIn (Sep O) f
  Proof.
O: Subuniverse
X, Y: Type
f: X -> Y
H: MapIn O (diagonal f)
MapIn (Sep O) f
    intros x1 u v.
O: Subuniverse
X, Y: Type
f: X -> Y
H: MapIn O (diagonal f)
x1: Y
u, v: hfiber f x1
In O (u = v)
    destruct v as [x2 p].
O: Subuniverse
X, Y: Type
f: X -> Y
H: MapIn O (diagonal f)
x1: Y
u: hfiber f x1
x2: X
p: f x2 = x1
In O (u = (x2; p))
    destruct p.
O: Subuniverse
X, Y: Type
f: X -> Y
H: MapIn O (diagonal f)
x2: X
u: hfiber f (f x2)
In O (u = (x2; 1))
    exact (inO_equiv_inO' _ (hfiber_diagonal f (u.1; x2; u.2))).
  Defined.

End Diagonal.

(** Lemma 2.15 of CORS: If [O] is accessible, so is [Sep O].  Its generators are the suspension of those of [O], in the following sense: *)
Definition susp_localgen (f : LocalGenerators@{a}) : LocalGenerators@{a}.
f: LocalGenerators
LocalGenerators
Proof.
f: LocalGenerators
LocalGenerators
  econstructor; intros i.
f: LocalGenerators
i: ?lgen_indices
?lgen_domain i -> ?lgen_codomain i
  exact (functor_susp (f i)).
Defined.

Instance isaccrsu_sep (O : Subuniverse) `{IsAccRSU O}
  : IsAccRSU (Sep O).
O: Subuniverse
H: IsAccRSU O
IsAccRSU (Sep O)
Proof.
O: Subuniverse
H: IsAccRSU O
IsAccRSU (Sep O)
  exists (susp_localgen (acc_lgen O)).
O: Subuniverse
H: IsAccRSU O
forall X : Type,
In (Sep O) X <-> IsLocal_Internal.IsLocal (susp_localgen (acc_lgen O)) X
  intros A; split; intros A_inO.
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In (Sep O) A
IsLocal_Internal.IsLocal (susp_localgen (acc_lgen O)) A
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: IsLocal_Internal.IsLocal (susp_localgen (acc_lgen O)) A
In (Sep O) A
  {
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In (Sep O) A
IsLocal_Internal.IsLocal (susp_localgen (acc_lgen O)) A intros i.
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (susp_localgen (acc_lgen O))
ooExtendableAlong (susp_localgen (acc_lgen O) i)
  (fun _ : lgen_codomain (susp_localgen (acc_lgen O)) i => A)
    apply (ooextendable_iff_functor_susp (acc_lgen O i)).
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (susp_localgen (acc_lgen O))
forall NS : A * A,
ooExtendableAlong (acc_lgen O i)
  (fun x : lgen_codomain (acc_lgen O) i =>
   DPath (fun _ : lgen_codomain (susp_localgen (acc_lgen O)) i => A)
     (merid x) (fst NS) (snd NS))  
    intros [x y].
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (susp_localgen (acc_lgen O))
x, y: A
ooExtendableAlong (acc_lgen O i)
  (fun x0 : lgen_codomain (acc_lgen O) i =>
   DPath (fun _ : lgen_codomain (susp_localgen (acc_lgen O)) i => A)
     (merid x0) (fst (x, y)) (snd (x, y))) cbn in *.
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: forall x0 y0 : A, In O (x0 = y0)
i: lgen_indices (acc_lgen O)
x, y: A
ooExtendableAlong (acc_lgen O i)
  (fun x0 : lgen_codomain (acc_lgen O) i =>
   transport (fun _ : Susp (lgen_codomain (acc_lgen O) i) => A) (merid x0) x =
   y)
    refine (ooextendable_postcompose' _ _ _ _ _).
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: forall x0 y0 : A, In O (x0 = y0)
i: lgen_indices (acc_lgen O)
x, y: A
forall b : lgen_codomain (acc_lgen O) i,
?Goal0 b <~>
transport (fun _ : Susp (lgen_codomain (acc_lgen O) i) => A) (merid b) x = y
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: forall x0 y0 : A, In O (x0 = y0)
i: lgen_indices (acc_lgen O)
x, y: A
ooExtendableAlong (acc_lgen O i) ?Goal0
    2:apply inO_iff_islocal; exact (A_inO x y).
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: forall x0 y0 : A, In O (x0 = y0)
i: lgen_indices (acc_lgen O)
x, y: A
forall b : lgen_codomain (acc_lgen O) i,
(fun _ : lgen_codomain (acc_lgen O) i => x = y) b <~>
transport (fun _ : Susp (lgen_codomain (acc_lgen O) i) => A) (merid b) x = y
    intros b.
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: forall x0 y0 : A, In O (x0 = y0)
i: lgen_indices (acc_lgen O)
x, y: A
b: lgen_codomain (acc_lgen O) i
(fun _ : lgen_codomain (acc_lgen O) i => x = y) b <~>
transport (fun _ : Susp (lgen_codomain (acc_lgen O) i) => A) (merid b) x = y
    exact dp_const. }
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: IsLocal_Internal.IsLocal (susp_localgen (acc_lgen O)) A
In (Sep O) A
  {
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: IsLocal_Internal.IsLocal (susp_localgen (acc_lgen O)) A
In (Sep O) A intros x y.
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: IsLocal_Internal.IsLocal (susp_localgen (acc_lgen O)) A
x, y: A
In O (x = y)
    apply (inO_iff_islocal O); intros i.
O: Subuniverse
H: IsAccRSU O
A: Type
A_inO: IsLocal_Internal.IsLocal (susp_localgen (acc_lgen O)) A
x, y: A
i: lgen_indices (acc_lgen O)
ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => x = y)
    specialize (A_inO i).
O: Subuniverse
H: IsAccRSU O
A: Type
i: lgen_indices (acc_lgen O)
A_inO: ooExtendableAlong (susp_localgen (acc_lgen O) i)
  (fun _ : lgen_codomain (susp_localgen (acc_lgen O)) i => A)
x, y: A
ooExtendableAlong (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => x = y)
    refine (ooextendable_postcompose' _ _ _ _ _).
O: Subuniverse
H: IsAccRSU O
A: Type
i: lgen_indices (acc_lgen O)
A_inO: ooExtendableAlong (susp_localgen (acc_lgen O) i)
  (fun _ : lgen_codomain (susp_localgen (acc_lgen O)) i => A)
x, y: A
forall b : lgen_codomain (acc_lgen O) i, ?Goal b <~> x = y
O: Subuniverse
H: IsAccRSU O
A: Type
i: lgen_indices (acc_lgen O)
A_inO: ooExtendableAlong (susp_localgen (acc_lgen O) i)
  (fun _ : lgen_codomain (susp_localgen (acc_lgen O)) i => A)
x, y: A
ooExtendableAlong (acc_lgen O i) ?Goal
    2:exact (fst (ooextendable_iff_functor_susp (acc_lgen O i) _) A_inO (x,y)).
O: Subuniverse
H: IsAccRSU O
A: Type
i: lgen_indices (acc_lgen O)
A_inO: ooExtendableAlong (susp_localgen (acc_lgen O) i)
  (fun _ : lgen_codomain (susp_localgen (acc_lgen O)) i => A)
x, y: A
forall b : lgen_codomain (acc_lgen O) i,
(fun x0 : lgen_codomain (acc_lgen O) i =>
 DPath (fun _ : lgen_codomain (susp_localgen (acc_lgen O)) i => A) 
   (merid x0) (fst (x, y)) (snd (x, y)))
  b <~>
x = y
    intros b.
O: Subuniverse
H: IsAccRSU O
A: Type
i: lgen_indices (acc_lgen O)
A_inO: ooExtendableAlong (susp_localgen (acc_lgen O) i)
  (fun _ : lgen_codomain (susp_localgen (acc_lgen O)) i => A)
x, y: A
b: lgen_codomain (acc_lgen O) i
(fun x0 : lgen_codomain (acc_lgen O) i =>
 DPath (fun _ : lgen_codomain (susp_localgen (acc_lgen O)) i => A) 
   (merid x0) (fst (x, y)) (snd (x, y)))
  b <~>
x = y
    symmetry; exact dp_const. }
Defined.

Definition susp_nullgen (S : NullGenerators@{a}) : NullGenerators@{a}.
S: NullGenerators
NullGenerators
Proof.
S: NullGenerators
NullGenerators
  econstructor; intros i.
S: NullGenerators
i: ?ngen_indices
Type
  exact (Susp (S i)).
Defined.

Instance isaccmodality_sep (O : Subuniverse) `{IsAccModality O}
  : IsAccModality (Sep O).
O: Subuniverse
H: IsAccModality O
IsAccModality (Sep O)
Proof.
O: Subuniverse
H: IsAccModality O
IsAccModality (Sep O)
  exists (susp_nullgen (acc_ngen O)).
O: Subuniverse
H: IsAccModality O
forall X : Type,
In (Sep O) X <-> IsNull_Internal.IsNull (susp_nullgen (acc_ngen O)) X
  intros A; split; intros A_inO.
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: In (Sep O) A
IsNull_Internal.IsNull (susp_nullgen (acc_ngen O)) A
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: IsNull_Internal.IsNull (susp_nullgen (acc_ngen O)) A
In (Sep O) A
  {
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: In (Sep O) A
IsNull_Internal.IsNull (susp_nullgen (acc_ngen O)) A intros i.
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (null_to_local_generators (susp_nullgen (acc_ngen O)))
ooExtendableAlong (null_to_local_generators (susp_nullgen (acc_ngen O)) i)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
    apply (ooextendable_compose _ (functor_susp (fun _:acc_ngen O i => tt)) (fun _:Susp Unit => tt)).
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (null_to_local_generators (susp_nullgen (acc_ngen O)))
ooExtendableAlong (fun _ : Susp Unit => tt)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (null_to_local_generators (susp_nullgen (acc_ngen O)))
ooExtendableAlong (functor_susp (fun _ : acc_ngen O i => tt))
  (fun _ : Susp Unit => A)
    1:apply ooextendable_equiv, isequiv_contr_contr.
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (null_to_local_generators (susp_nullgen (acc_ngen O)))
ooExtendableAlong (functor_susp (fun _ : acc_ngen O i => tt))
  (fun _ : Susp Unit => A)
    apply (ooextendable_iff_functor_susp (fun _:acc_ngen O i => tt)).
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (null_to_local_generators (susp_nullgen (acc_ngen O)))
forall NS : A * A,
ooExtendableAlong (fun _ : acc_ngen O i => tt)
  (fun x : Unit => DPath (fun _ : Susp Unit => A) (merid x) (fst NS) (snd NS))  
    intros [x y].
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (null_to_local_generators (susp_nullgen (acc_ngen O)))
x, y: A
ooExtendableAlong (fun _ : acc_ngen O i => tt)
  (fun x0 : Unit =>
   DPath (fun _ : Susp Unit => A) (merid x0) (fst (x, y)) (snd (x, y)))
    refine (ooextendable_postcompose' _ _ _ _ _).
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (null_to_local_generators (susp_nullgen (acc_ngen O)))
x, y: A
forall b : Unit,
?Goal0 b <~>
DPath (fun _ : Susp Unit => A) (merid b) (fst (x, y)) (snd (x, y))
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (null_to_local_generators (susp_nullgen (acc_ngen O)))
x, y: A
ooExtendableAlong (fun _ : acc_ngen O i => tt) ?Goal0
    2:apply inO_iff_isnull; exact (A_inO x y).
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (null_to_local_generators (susp_nullgen (acc_ngen O)))
x, y: A
forall b : Unit,
(fun _ : lgen_codomain (null_to_local_generators (acc_ngen O)) i => x = y) b <~>
DPath (fun _ : Susp Unit => A) (merid b) (fst (x, y)) (snd (x, y))
    intros b.
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: In (Sep O) A
i: lgen_indices (null_to_local_generators (susp_nullgen (acc_ngen O)))
x, y: A
b: Unit
(fun _ : lgen_codomain (null_to_local_generators (acc_ngen O)) i => x = y) b <~>
DPath (fun _ : Susp Unit => A) (merid b) (fst (x, y)) (snd (x, y))
    exact dp_const. }
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: IsNull_Internal.IsNull (susp_nullgen (acc_ngen O)) A
In (Sep O) A
  {
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: IsNull_Internal.IsNull (susp_nullgen (acc_ngen O)) A
In (Sep O) A intros x y.
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: IsNull_Internal.IsNull (susp_nullgen (acc_ngen O)) A
x, y: A
In O (x = y)
    apply (inO_iff_isnull O); intros i.
O: Subuniverse
H: IsAccModality O
A: Type
A_inO: IsNull_Internal.IsNull (susp_nullgen (acc_ngen O)) A
x, y: A
i: lgen_indices (null_to_local_generators (acc_ngen O))
ooExtendableAlong (null_to_local_generators (acc_ngen O) i)
  (fun _ : lgen_codomain (null_to_local_generators (acc_ngen O)) i => x = y)
    specialize (A_inO i).
O: Subuniverse
H: IsAccModality O
A: Type
i: lgen_indices (null_to_local_generators (acc_ngen O))
A_inO: ooExtendableAlong (null_to_local_generators (susp_nullgen (acc_ngen O)) i)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
x, y: A
ooExtendableAlong (null_to_local_generators (acc_ngen O) i)
  (fun _ : lgen_codomain (null_to_local_generators (acc_ngen O)) i => x = y)
    assert (ee : ooExtendableAlong (functor_susp (fun _:acc_ngen O i => tt)) (fun _ => A)).
O: Subuniverse
H: IsAccModality O
A: Type
i: lgen_indices (null_to_local_generators (acc_ngen O))
A_inO: ooExtendableAlong (null_to_local_generators (susp_nullgen (acc_ngen O)) i)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
x, y: A
ooExtendableAlong (functor_susp (fun _ : acc_ngen O i => tt))
  (fun _ : Susp Unit => A)
O: Subuniverse
H: IsAccModality O
A: Type
i: lgen_indices (null_to_local_generators (acc_ngen O))
A_inO: ooExtendableAlong (null_to_local_generators (susp_nullgen (acc_ngen O)) i)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
x, y: A
ee: ooExtendableAlong (functor_susp (fun _ : acc_ngen O i => tt))
  (fun _ : Susp Unit => A)
ooExtendableAlong (null_to_local_generators (acc_ngen O) i)
  (fun _ : lgen_codomain (null_to_local_generators (acc_ngen O)) i => x = y)
    {
O: Subuniverse
H: IsAccModality O
A: Type
i: lgen_indices (null_to_local_generators (acc_ngen O))
A_inO: ooExtendableAlong (null_to_local_generators (susp_nullgen (acc_ngen O)) i)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
x, y: A
ooExtendableAlong (functor_susp (fun _ : acc_ngen O i => tt))
  (fun _ : Susp Unit => A) refine (cancelL_ooextendable _ _ (fun _ => tt) _ A_inO).
O: Subuniverse
H: IsAccModality O
A: Type
i: lgen_indices (null_to_local_generators (acc_ngen O))
A_inO: ooExtendableAlong (null_to_local_generators (susp_nullgen (acc_ngen O)) i)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
x, y: A
ooExtendableAlong (fun _ : Susp Unit => tt)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
      apply ooextendable_equiv.
O: Subuniverse
H: IsAccModality O
A: Type
i: lgen_indices (null_to_local_generators (acc_ngen O))
A_inO: ooExtendableAlong (null_to_local_generators (susp_nullgen (acc_ngen O)) i)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
x, y: A
IsEquiv (fun _ : Susp Unit => tt)
      apply isequiv_contr_contr. }
O: Subuniverse
H: IsAccModality O
A: Type
i: lgen_indices (null_to_local_generators (acc_ngen O))
A_inO: ooExtendableAlong (null_to_local_generators (susp_nullgen (acc_ngen O)) i)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
x, y: A
ee: ooExtendableAlong (functor_susp (fun _ : acc_ngen O i => tt))
  (fun _ : Susp Unit => A)
ooExtendableAlong (null_to_local_generators (acc_ngen O) i)
  (fun _ : lgen_codomain (null_to_local_generators (acc_ngen O)) i => x = y)
    assert (e := fst (ooextendable_iff_functor_susp (fun _:acc_ngen O i => tt) _) ee (x,y)).
O: Subuniverse
H: IsAccModality O
A: Type
i: lgen_indices (null_to_local_generators (acc_ngen O))
A_inO: ooExtendableAlong (null_to_local_generators (susp_nullgen (acc_ngen O)) i)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
x, y: A
ee: ooExtendableAlong (functor_susp (fun _ : acc_ngen O i => tt))
  (fun _ : Susp Unit => A)
e: ooExtendableAlong (fun _ : acc_ngen O i => tt)
  (fun x0 : Unit =>
   DPath (fun _ : Susp Unit => A) (merid x0) (fst (x, y)) (snd (x, y)))
ooExtendableAlong (null_to_local_generators (acc_ngen O) i)
  (fun _ : lgen_codomain (null_to_local_generators (acc_ngen O)) i => x = y)
    cbn in e.
O: Subuniverse
H: IsAccModality O
A: Type
i: lgen_indices (null_to_local_generators (acc_ngen O))
A_inO: ooExtendableAlong (null_to_local_generators (susp_nullgen (acc_ngen O)) i)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
x, y: A
ee: ooExtendableAlong (functor_susp (fun _ : acc_ngen O i => tt))
  (fun _ : Susp Unit => A)
e: ooExtendableAlong (fun _ : acc_ngen O i => tt)
  (fun x0 : Unit => transport (fun _ : Susp Unit => A) (merid x0) x = y)
ooExtendableAlong (null_to_local_generators (acc_ngen O) i)
  (fun _ : lgen_codomain (null_to_local_generators (acc_ngen O)) i => x = y)
    refine (ooextendable_postcompose' _ _ _ _ e).
O: Subuniverse
H: IsAccModality O
A: Type
i: lgen_indices (null_to_local_generators (acc_ngen O))
A_inO: ooExtendableAlong (null_to_local_generators (susp_nullgen (acc_ngen O)) i)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
x, y: A
ee: ooExtendableAlong (functor_susp (fun _ : acc_ngen O i => tt))
  (fun _ : Susp Unit => A)
e: ooExtendableAlong (fun _ : acc_ngen O i => tt)
  (fun x0 : Unit => transport (fun _ : Susp Unit => A) (merid x0) x = y)
forall b : Unit, transport (fun _ : Susp Unit => A) (merid b) x = y <~> x = y
    intros b.
O: Subuniverse
H: IsAccModality O
A: Type
i: lgen_indices (null_to_local_generators (acc_ngen O))
A_inO: ooExtendableAlong (null_to_local_generators (susp_nullgen (acc_ngen O)) i)
  (fun
     _ : lgen_codomain (null_to_local_generators (susp_nullgen (acc_ngen O)))
           i =>
   A)
x, y: A
ee: ooExtendableAlong (functor_susp (fun _ : acc_ngen O i => tt))
  (fun _ : Susp Unit => A)
e: ooExtendableAlong (fun _ : acc_ngen O i => tt)
  (fun x0 : Unit => transport (fun _ : Susp Unit => A) (merid x0) x = y)
b: Unit
transport (fun _ : Susp Unit => A) (merid b) x = y <~> x = y
    symmetry; exact dp_const. }
Defined.

(** Remark 2.16(1) of CORS *)
Instance O_leq_SepO (O : ReflectiveSubuniverse)
  : O <= Sep O.
O: ReflectiveSubuniverse
O <= Sep O
Proof.
O: ReflectiveSubuniverse
O <= Sep O
  intros A ? x y; exact _.
Defined.

(** Part of Remark 2.16(2) of CORS *)
Definition in_SepO_embedding (O : Subuniverse)
           {A B : Type} (i : A -> B) `{IsEmbedding i} `{In (Sep O) B}
  : In (Sep O) A.
O: Subuniverse
A, B: Type
i: A -> B
IsEmbedding0: IsEmbedding i
H: In (Sep O) B
In (Sep O) A
Proof.
O: Subuniverse
A, B: Type
i: A -> B
IsEmbedding0: IsEmbedding i
H: In (Sep O) B
In (Sep O) A
  intros x y.
O: Subuniverse
A, B: Type
i: A -> B
IsEmbedding0: IsEmbedding i
H: In (Sep O) B
x, y: A
In O (x = y)
  exact (inO_equiv_inO' _ (equiv_ap_isembedding i x y)^-1).
Defined.

(* As a special case, if X embeds into an n-type for n >= -1 then X is an n-type. Note that this doesn't hold for n = -2. *)
Corollary istrunc_embedding_trunc {X Y : Type} {n : trunc_index} `{istr : IsTrunc n.+1 Y}
      (i : X -> Y) `{isem : IsEmbedding i} : IsTrunc n.+1 X.
X, Y: Type
n: trunc_index
istr: IsTrunc n.+1 Y
i: X -> Y
isem: IsEmbedding i
IsTrunc n.+1 X
Proof.
X, Y: Type
n: trunc_index
istr: IsTrunc n.+1 Y
i: X -> Y
isem: IsEmbedding i
IsTrunc n.+1 X
  apply istrunc_S.
X, Y: Type
n: trunc_index
istr: IsTrunc n.+1 Y
i: X -> Y
isem: IsEmbedding i
forall x y : X, IsTrunc n (x = y)
  exact (@in_SepO_embedding (Tr n) _ _ i isem istr).
Defined.

Instance in_SepO_hprop (O : ReflectiveSubuniverse)
       {A : Type} `{IsHProp A}
  : In (Sep O) A.
O: ReflectiveSubuniverse
A: Type
IsHProp0: IsHProp A
In (Sep O) A
Proof.
O: ReflectiveSubuniverse
A: Type
IsHProp0: IsHProp A
In (Sep O) A
  srapply (in_SepO_embedding O (const_tt _)).
O: ReflectiveSubuniverse
A: Type
IsHProp0: IsHProp A
In (Sep O) Unit
  intros x y; exact _.
Defined.


(** Remark 2.16(4) of CORS *)
Definition sigma_closed_SepO (O : Modality) {A : Type} (B : A -> Type)
           `{A_inO : In (Sep O) A} `{B_inO : forall a, In (Sep O) (B a)}
  : In (Sep O) (sig B).
O: Modality
A: Type
B: A -> Type
A_inO: In (Sep O) A
B_inO: forall a : A, In (Sep O) (B a)
In (Sep O) {x : _ & B x}
Proof.
O: Modality
A: Type
B: A -> Type
A_inO: In (Sep O) A
B_inO: forall a : A, In (Sep O) (B a)
In (Sep O) {x : _ & B x}
  intros [x u] [y v].
O: Modality
A: Type
B: A -> Type
A_inO: In (Sep O) A
B_inO: forall a : A, In (Sep O) (B a)
x: A
u: B x
y: A
v: B y
In O ((x; u) = (y; v))
  specialize (A_inO x y).
O: Modality
A: Type
B: A -> Type
x, y: A
A_inO: In O (x = y)
B_inO: forall a : A, In (Sep O) (B a)
u: B x
v: B y
In O ((x; u) = (y; v))
  pose proof (fun p:x=y => B_inO y (p # u) v).
O: Modality
A: Type
B: A -> Type
x, y: A
A_inO: In O (x = y)
B_inO: forall a : A, In (Sep O) (B a)
u: B x
v: B y
X: forall p : x = y, In O (transport B p u = v)
In O ((x; u) = (y; v))
  pose @inO_sigma.  (* Speed up typeclass search. *)
O: Modality
A: Type
B: A -> Type
x, y: A
A_inO: In O (x = y)
B_inO: forall a : A, In (Sep O) (B a)
u: B x
v: B y
X: forall p : x = y, In O (transport B p u = v)
i:= inO_sigma: forall (O0 : Modality) (A0 : Type) (B0 : A0 -> Type),
In O0 A0 -> (forall a : A0, In O0 (B0 a)) -> In O0 {x0 : A0 & B0 x0}
In O ((x; u) = (y; v))
  exact (inO_equiv_inO' _ (equiv_path_sigma B _ _)).
Defined.

(** Lemma 2.17 of CORS *)
Instance issurjective_to_SepO (O : ReflectiveSubuniverse) (X : Type)
           `{Reflects (Sep O) X}
  : IsSurjection (to (Sep O) X).
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
IsConnMap (Tr (-1)) (to (Sep O) X)
Proof.
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
IsConnMap (Tr (-1)) (to (Sep O) X)
  pose (im := himage (to (Sep O) X)).
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
IsConnMap (Tr (-1)) (to (Sep O) X)
  pose proof (in_SepO_embedding O (factor2 im)).
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
IsConnMap (Tr (-1)) (to (Sep O) X)
  pose (s := O_rec (factor1 im)).
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
s:= O_rec (factor1 im): O_reflector (Sep O) X -> im
IsConnMap (Tr (-1)) (to (Sep O) X)
  assert (h : factor2 im o s == idmap).
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
s:= O_rec (factor1 im): O_reflector (Sep O) X -> im
(fun x : O_reflector (Sep O) X => factor2 im (s x)) == idmap
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
s:= O_rec (factor1 im): O_reflector (Sep O) X -> im
h: factor2 im o s == idmap
IsConnMap (Tr (-1)) (to (Sep O) X)
  -
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
s:= O_rec (factor1 im): O_reflector (Sep O) X -> im
(fun x : O_reflector (Sep O) X => factor2 im (s x)) == idmap apply O_indpaths; intros x; subst s.
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
x: X
factor2 im (O_rec (factor1 im) (to (Sep O) X x)) = to (Sep O) X x
    rewrite O_rec_beta.
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
x: X
factor2 im (factor1 im x) = to (Sep O) X x
    apply fact_factors.
  -
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
s:= O_rec (factor1 im): O_reflector (Sep O) X -> im
h: factor2 im o s == idmap
IsConnMap (Tr (-1)) (to (Sep O) X) apply BuildIsSurjection.
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
s:= O_rec (factor1 im): O_reflector (Sep O) X -> im
h: factor2 im o s == idmap
forall b : O_reflector (Sep O) X, merely (hfiber (to (Sep O) X) b)
    intros z.
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
s:= O_rec (factor1 im): O_reflector (Sep O) X -> im
h: factor2 im o s == idmap
z: O_reflector (Sep O) X
merely (hfiber (to (Sep O) X) z)
    specialize (h z); cbn in h.
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
s:= O_rec (factor1 im): O_reflector (Sep O) X -> im
z: O_reflector (Sep O) X
h: (s z).1 = z
merely (hfiber (to (Sep O) X) z)
    set (w := s z) in *.
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
s:= O_rec (factor1 im): O_reflector (Sep O) X -> im
z: O_reflector (Sep O) X
w:= s z: im
h: w.1 = z
merely (hfiber (to (Sep O) X) z)
    destruct w as [w1 w2].
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
s:= O_rec (factor1 im): O_reflector (Sep O) X -> im
z, w1: O_reflector (Sep O) X
w2: Tr (-1) (hfiber (to (Sep O) X) w1)
h: (w1; w2).1 = z
merely (hfiber (to (Sep O) X) z)
    destruct h.
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
im:= himage (to (Sep O) X): Factorization (@IsConnMap (Tr (-1))) (@MapIn (Tr (-1))) (to (Sep O) X)
X0: In (Sep O) im
s:= O_rec (factor1 im): O_reflector (Sep O) X -> im
w1: O_reflector (Sep O) X
w2: Tr (-1) (hfiber (to (Sep O) X) w1)
merely (hfiber (to (Sep O) X) (w1; w2).1)
    exact w2.
Defined.

(** Proposition 2.18 of CORS. *)
Definition almost_inSepO_typeO@{i j} `{Univalence}
           (O : ReflectiveSubuniverse) (A B : Type_@{i j} O)
  : { Z : Type@{i} & In O Z * (Z <~> (A = B)) }.
H: Univalence
O: ReflectiveSubuniverse
A, B: Type_ O
{Z : Type & In O Z * (Z <~> A = B)}
Proof.
H: Univalence
O: ReflectiveSubuniverse
A, B: Type_ O
{Z : Type & In O Z * (Z <~> A = B)}
  exists (A <~> B); split.
H: Univalence
O: ReflectiveSubuniverse
A, B: Type_ O
In O (A <~> B)
H: Univalence
O: ReflectiveSubuniverse
A, B: Type_ O
(A <~> B) <~> A = B
  -
H: Univalence
O: ReflectiveSubuniverse
A, B: Type_ O
In O (A <~> B) exact _.
  -
H: Univalence
O: ReflectiveSubuniverse
A, B: Type_ O
(A <~> B) <~> A = B refine (equiv_path_TypeO O A B oE _).
H: Univalence
O: ReflectiveSubuniverse
A, B: Type_ O
(A <~> B) <~> A.1 = B.1
    apply equiv_path_universe.
Defined.

(** Lemma 2.21 of CORS *)
Instance inSepO_sigma (O : ReflectiveSubuniverse)
       {X : Type} {P : X -> Type} `{In (Sep O) X} `{forall x, In O (P x)}
  : In (Sep O) (sig P).
O: ReflectiveSubuniverse
X: Type
P: X -> Type
H: In (Sep O) X
H0: forall x : X, In O (P x)
In (Sep O) {x : _ & P x}
Proof.
O: ReflectiveSubuniverse
X: Type
P: X -> Type
H: In (Sep O) X
H0: forall x : X, In O (P x)
In (Sep O) {x : _ & P x}
  intros u v.
O: ReflectiveSubuniverse
X: Type
P: X -> Type
H: In (Sep O) X
H0: forall x : X, In O (P x)
u, v: {x : _ & P x}
In O (u = v)
  exact (inO_equiv_inO' _ (equiv_path_sigma P _ _)).
Defined.

(** Proposition 2.22 of CORS (in funext-free form). *)
Instance reflectsD_SepO (O : ReflectiveSubuniverse)
       {X : Type} `{Reflects (Sep O) X}
  : ReflectsD (Sep O) O X.
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
ReflectsD (Sep O) O X
Proof.
O: ReflectiveSubuniverse
X: Type
H: PreReflects (Sep O) X
H0: Reflects (Sep O) X
ReflectsD (Sep O) O X
  srapply reflectsD_from_inO_sigma.
Defined.

(** Once we know that [Sep O] is a reflective subuniverse, this will mean that [O << Sep O]. *)

(** And now the version with funext. *)
Definition isequiv_toSepO_inO `{Funext} (O : ReflectiveSubuniverse)
           {X : Type} `{Reflects (Sep O) X}
           (P : O_reflector (Sep O) X -> Type) `{forall x, In O (P x)}
  : IsEquiv (fun g : (forall y, P y) => g o to (Sep O) X)
  := isequiv_ooextendable _ _ (extendable_to_OO P).

Definition equiv_toSepO_inO `{Funext} (O : ReflectiveSubuniverse)
           {X : Type} `{Reflects (Sep O) X}
           (P : O_reflector (Sep O) X -> Type) `{forall x, In O (P x)}
  : (forall y, P y) <~> (forall x, P (to (Sep O) X x))
  := Build_Equiv _ _ _ (isequiv_toSepO_inO O P).

(** TODO: Actually prove this, and put it somewhere more appropriate. *)
Section JoinConstruction.
  Universes i j.
  Context {X : Type@{i}} {Y : Type@{j}} (f : X -> Y)
          (ls : forall (y1 y2 : Y),
              @sig@{j j} Type@{i} (fun (Z : Type@{i}) => Equiv@{i j} Z (y1 = y2))).
  Definition jc_image@{} : Type@{i}.
X, Y: Type
f: X -> Y
ls: forall y1 y2 : Y, {Z : Type & Z <~> y1 = y2}
Type Admitted.
  Definition jc_factor1@{} : X -> jc_image.
X, Y: Type
f: X -> Y
ls: forall y1 y2 : Y, {Z : Type & Z <~> y1 = y2}
X -> jc_image Admitted.
  Definition jc_factor2@{} : jc_image -> Y.
X, Y: Type
f: X -> Y
ls: forall y1 y2 : Y, {Z : Type & Z <~> y1 = y2}
jc_image -> Y Admitted.
  Definition jc_factors@{} : jc_factor2 o jc_factor1 == f.
X, Y: Type
f: X -> Y
ls: forall y1 y2 : Y, {Z : Type & Z <~> y1 = y2}
jc_factor2 o jc_factor1 == f Admitted.
  #[export] Instance jc_factor1_issurj@{} : IsSurjection jc_factor1.
X, Y: Type
f: X -> Y
ls: forall y1 y2 : Y, {Z : Type & Z <~> y1 = y2}
IsConnMap (Tr (-1)) jc_factor1 Admitted.
  #[export] Instance jc_factor2_isemb : IsEmbedding jc_factor2.
X, Y: Type
f: X -> Y
ls: forall y1 y2 : Y, {Z : Type & Z <~> y1 = y2}
IsEmbedding jc_factor2 Admitted.
End JoinConstruction.

(** We'd like to say that the universe of [O]-modal types is [O]-separated, i.e. belongs to [Sep O].  But since a given subuniverse like [Sep O] lives only on a single universe size, trying to say that in the naive way yields a universe inconsistency. *)
Fail Goal forall (O : ReflectiveSubuniverse), In (Sep O) (Type_ O).

(** Instead, we do as in Lemma 2.19 of CORS and prove the morally-equivalent "descent" property, using Lemma 2.18 and the join construction. *)
Instance SepO_lex_leq `{Univalence}
       (O : ReflectiveSubuniverse) {X : Type} `{Reflects (Sep O) X}
  : Descends (Sep O) O X.
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
Descends (Sep O) O X
Proof.
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
Descends (Sep O) O X
  assert (e : forall (P : X -> Type_ O),
             { Q : (O_reflector (Sep O) X -> Type_ O) &
                   forall x, Q (to (Sep O) X x) <~> P x }).
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
forall P : X -> Type_ O,
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
e: forall P : X -> Type_ O,
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
Descends (Sep O) O X
  2:{
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
e: forall P : X -> Type_ O,
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
Descends (Sep O) O X unshelve econstructor; intros P' P_inO;
      pose (P := fun x => (P' x; P_inO x) : Type_ O);
      pose (ee := e P).
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
e: forall P0 : X -> Type_ O,
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P0 x}
P': X -> Type
P_inO: forall x : X, In O (P' x)
P:= fun x : X => (P' x; P_inO x) : Type_ O: X -> Type_ O
ee:= e P: {Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
O_reflector (Sep O) X -> Type
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
e: forall P0 : X -> Type_ O,
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P0 x}
P': X -> Type
P_inO: forall x : X, In O (P' x)
P:= fun x : X => (P' x; P_inO x) : Type_ O: X -> Type_ O
ee:= e P: {Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
forall x : O_reflector (Sep O) X,
In O
  ((fun (P'0 : X -> Type) (P_inO0 : forall x0 : X, In O (P'0 x0)) =>
    let P0 := fun x0 : X => (P'0 x0; P_inO0 x0) : Type_ O in
    let ee0 := e P0 in ?Goal0@{P':=P'0; P_inO:=P_inO0}) P' P_inO x)
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
e: forall P0 : X -> Type_ O,
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P0 x}
P': X -> Type
P_inO: forall x : X, In O (P' x)
P:= fun x : X => (P' x; P_inO x) : Type_ O: X -> Type_ O
ee:= e P: {Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
forall x : X,
(fun (P'0 : X -> Type) (P_inO0 : forall x0 : X, In O (P'0 x0)) =>
 let P0 := fun x0 : X => (P'0 x0; P_inO0 x0) : Type_ O in
 let ee0 := e P0 in ?Goal0@{P':=P'0; P_inO:=P_inO0}) P' P_inO
  (to (Sep O) X x) <~>
P' x
      -
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
e: forall P0 : X -> Type_ O,
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P0 x}
P': X -> Type
P_inO: forall x : X, In O (P' x)
P:= fun x : X => (P' x; P_inO x) : Type_ O: X -> Type_ O
ee:= e P: {Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
O_reflector (Sep O) X -> Type exact ee.1.
      -
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
e: forall P0 : X -> Type_ O,
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P0 x}
P': X -> Type
P_inO: forall x : X, In O (P' x)
P:= fun x : X => (P' x; P_inO x) : Type_ O: X -> Type_ O
ee:= e P: {Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
forall x : O_reflector (Sep O) X,
In O
  ((fun (P'0 : X -> Type) (P_inO0 : forall x0 : X, In O (P'0 x0)) =>
    let P0 := fun x0 : X => (P'0 x0; P_inO0 x0) : Type_ O in
    let ee0 := e P0 in
    fun x0 : O_reflector (Sep O) X => TypeO_pr1 O (ee0.1 x0)) P' P_inO x) simpl; exact _.
      -
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
e: forall P0 : X -> Type_ O,
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P0 x}
P': X -> Type
P_inO: forall x : X, In O (P' x)
P:= fun x : X => (P' x; P_inO x) : Type_ O: X -> Type_ O
ee:= e P: {Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
forall x : X,
(fun (P'0 : X -> Type) (P_inO0 : forall x0 : X, In O (P'0 x0)) =>
 let P0 := fun x0 : X => (P'0 x0; P_inO0 x0) : Type_ O in
 let ee0 := e P0 in fun x0 : O_reflector (Sep O) X => TypeO_pr1 O (ee0.1 x0))
  P' P_inO (to (Sep O) X x) <~>
P' x intros x; cbn; apply ee.2. }
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
forall P : X -> Type_ O,
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
  intros P.
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
  assert (ls : forall A B : Type_ O, { Z : Type & Z <~> (A = B) }).
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
forall A B : Type_ O, {Z : Type & Z <~> A = B}
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
  {
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
forall A B : Type_ O, {Z : Type & Z <~> A = B} intros A B.
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
A, B: Type_ O
{Z : Type & Z <~> A = B}
    pose (q := almost_inSepO_typeO O A B).
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
A, B: Type_ O
q:= almost_inSepO_typeO O A B: {Z : Type & In O Z * (Z <~> A = B)}
{Z : Type & Z <~> A = B}
    exact (q.1; snd q.2). }
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
  pose (p := jc_factor2 P ls).
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
p:= jc_factor2 P ls: jc_image P ls -> Type_ O
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
  set (J := jc_image P ls) in p.
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
  assert (In (Sep O) J).
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
In (Sep O) J
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
X0: In (Sep O) J
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
  {
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
In (Sep O) J intros x y.
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
x, y: J
In O (x = y)
    pose (q := almost_inSepO_typeO O (p x) (p y)).
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
x, y: J
q:= almost_inSepO_typeO O (p x) (p y): {Z : Type & In O Z * (Z <~> p x = p y)}
In O (x = y)
    refine (inO_equiv_inO' q.1 _).
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
x, y: J
q:= almost_inSepO_typeO O (p x) (p y): {Z : Type & In O Z * (Z <~> p x = p y)}
q.1 <~> x = y
    refine (_ oE _).
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
x, y: J
q:= almost_inSepO_typeO O (p x) (p y): {Z : Type & In O Z * (Z <~> p x = p y)}
?Goal0 <~> x = y
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
x, y: J
q:= almost_inSepO_typeO O (p x) (p y): {Z : Type & In O Z * (Z <~> p x = p y)}
q.1 <~> ?Goal0
    -
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
x, y: J
q:= almost_inSepO_typeO O (p x) (p y): {Z : Type & In O Z * (Z <~> p x = p y)}
?Goal0 <~> x = y symmetry; srapply (equiv_ap_isembedding p).
    -
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
x, y: J
q:= almost_inSepO_typeO O (p x) (p y): {Z : Type & In O Z * (Z <~> p x = p y)}
q.1 <~> p x = p y exact (snd q.2). }
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
X0: In (Sep O) J
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
  pose (O_rec (O := Sep O) (jc_factor1 P ls)).
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
X0: In (Sep O) J
j:= O_rec (jc_factor1 P ls): O_reflector (Sep O) X -> jc_image P ls
{Q : O_reflector (Sep O) X -> Type_ O &
forall x : X, Q (to (Sep O) X x) <~> P x}
  exists (p o j).
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
p:= jc_factor2 P ls: J -> Type_ O
X0: In (Sep O) J
j:= O_rec (jc_factor1 P ls): O_reflector (Sep O) X -> jc_image P ls
forall x : X, p (j (to (Sep O) X x)) <~> P x
  intros x; subst p j.
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
X0: In (Sep O) J
x: X
jc_factor2 P ls (O_rec (jc_factor1 P ls) (to (Sep O) X x)) <~> P x
  rewrite O_rec_beta.
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
X0: In (Sep O) J
x: X
jc_factor2 P ls (jc_factor1 P ls x) <~> P x
  apply equiv_path.
H: Univalence
O: ReflectiveSubuniverse
X: Type
H0: PreReflects (Sep O) X
H1: Reflects (Sep O) X
P: X -> Type_ O
ls: forall A B : Type_ O, {Z : Type & Z <~> A = B}
J:= jc_image P ls: Type
X0: In (Sep O) J
x: X
jc_factor2 P ls (jc_factor1 P ls x) = P x
  exact ((jc_factors P ls x)..1).
Defined.

(** Once we know that [Sep O] is a reflective subuniverse, this will imply [O <<< Sep O], and that if [Sep O] is accessible (such as if [O] is) then [Type_ O] belongs to its accessible lifting (see [inO_TypeO_lex_leq]. *)


(** ** Reflectiveness of [Sep O] *)

(** TODO *)


(** ** Left-exactness properties *)

(** Nearly all of these are true in the generality of a pair of reflective subuniverses with [O <<< O'] and/or [O' <= Sep O], and as such can be found in [Descent.v]. *)