Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HFiber Extensions Limits.Pullback.
Require Import Modality Accessible Modalities.Localization.

Local Open Scope path_scope.
Local Open Scope subuniverse_scope.

(** * Descent between subuniverses *)

(** We study here a strengthening of the relation [O << O'] saying that [O]-modal type families descend along [O']-equivalences.  Pairs of reflective subuniverses with this relation share nearly all the properties of a reflective subuniverse [O] paired with its subuniverse [Sep O] of separated types (see [Separated.v]) and also many of those of a single left exact modality (see [Lex.v]).  Thus, many of the results herein generalize those of RSS for lex modalities and those of CORS for separated subuniverses.

Note that this kind of descent is not the same as the "modal descent" of Cherubini and Rijke.  When we get around to formalizing that, we may need to worry about disambiguating the names. *)

(** ** Definitions *)

(** This definition is an analogue of the statement of Lemma 2.19 of CORS, and of Theorem 3.1(xiii) of RSS.  Note that CORS Lemma 2.19 includes uniqueness of the extension, which we don't assert explicitly.  However, uniqueness follows from the [ReflectsD] parameter -- see [ooextendable_TypeO_lex_leq] below. *)
Class Descends@{i} (O' O : Subuniverse@{i}) (T : Type@{i})
      `{ReflectsD@{i} O' O T} :=
{
  OO_descend :
    forall (P : T -> Type@{i}) {P_inO : forall x, In O (P x)},
      O_reflector O' T -> Type@{i} ;
  OO_descend_inO ::
    forall (P : T -> Type@{i}) {P_inO : forall x, In O (P x)} (x : O_reflector O' T),
      In O (OO_descend P x) ;
  OO_descend_beta :
    forall (P : T -> Type@{i}) {P_inO : forall x, In O (P x)} (x : T),
      OO_descend P (to O' T x) <~> P x ;
}.

Arguments OO_descend O' O {T _ _ _} P {P_inO} x.
Arguments OO_descend_inO O' O {T _ _ _} P {P_inO} x.
Arguments OO_descend_beta O' O {T _ _ _} P {P_inO} x.

Class O_lex_leq (O1 O2 : ReflectiveSubuniverse) `{O1 << O2} :=
  O_lex_leq_descends :: forall A, Descends O2 O1 A.

Infix "<<<" := O_lex_leq : subuniverse_scope.

(** Unfortunately, it seems that generalizing binders don't work on notations: writing [`{O <<< O'}] doesn't automatically add the precondition [O << O'], although writing [`{O_lex_leq O O'}] does. *)

Definition O_lex_leq_eq {O1 O2 O3 : ReflectiveSubuniverse}
           `{O1 <=> O2} `{O2 << O3, O2 <<< O3}
           (Hstrong := O_strong_leq_trans_l O1 O2 O3)
  : O1 <<< O3.
O1, O2, O3: ReflectiveSubuniverse
H: O1 <=> O2
H0: O2 << O3
H1: O2 <<< O3
Hstrong:= O_strong_leq_trans_l O1 O2 O3: O1 << O3
O1 <<< O3
Proof.
O1, O2, O3: ReflectiveSubuniverse
H: O1 <=> O2
H0: O2 << O3
H1: O2 <<< O3
Hstrong:= O_strong_leq_trans_l O1 O2 O3: O1 << O3
O1 <<< O3
  intros A; unshelve econstructor; intros P P_inO1.
O1, O2, O3: ReflectiveSubuniverse
H: O1 <=> O2
H0: O2 << O3
H1: O2 <<< O3
Hstrong:= O_strong_leq_trans_l O1 O2 O3: O1 << O3
A: Type
P: A -> Type
P_inO1: forall x : A, In O1 (P x)
O_reflector O3 A -> Type
O1, O2, O3: ReflectiveSubuniverse
H: O1 <=> O2
H0: O2 << O3
H1: O2 <<< O3
Hstrong:= O_strong_leq_trans_l O1 O2 O3: O1 << O3
A: Type
P: A -> Type
P_inO1: forall x : A, In O1 (P x)
forall x : O_reflector O3 A,
In O1
  ((fun (P : A -> Type)
      (P_inO1 : forall x0 : A, In O1 (P x0)) => 
    ?Goal) P P_inO1 x)
O1, O2, O3: ReflectiveSubuniverse
H: O1 <=> O2
H0: O2 << O3
H1: O2 <<< O3
Hstrong:= O_strong_leq_trans_l O1 O2 O3: O1 << O3
A: Type
P: A -> Type
P_inO1: forall x : A, In O1 (P x)
forall x : A,
(fun (P : A -> Type)
   (P_inO1 : forall x0 : A, In O1 (P x0)) => 
 ?Goal) P P_inO1 (to O3 A x) <~> 
P x
  all:pose (P_inO2 := fun x => inO_leq O1 O2 _ (P_inO1 x)).
O1, O2, O3: ReflectiveSubuniverse
H: O1 <=> O2
H0: O2 << O3
H1: O2 <<< O3
Hstrong:= O_strong_leq_trans_l O1 O2 O3: O1 << O3
A: Type
P: A -> Type
P_inO1: forall x : A, In O1 (P x)
P_inO2:= fun x : A => inO_leq O1 O2 (P x) (P_inO1 x): forall x : A, In O2 (P x)
O_reflector O3 A -> Type
O1, O2, O3: ReflectiveSubuniverse
H: O1 <=> O2
H0: O2 << O3
H1: O2 <<< O3
Hstrong:= O_strong_leq_trans_l O1 O2 O3: O1 << O3
A: Type
P: A -> Type
P_inO1: forall x : A, In O1 (P x)
P_inO2:= fun x : A => inO_leq O1 O2 (P x) (P_inO1 x): forall x : A, In O2 (P x)
forall x : O_reflector O3 A,
In O1
  ((fun (P : A -> Type)
      (P_inO1 : forall x0 : A, In O1 (P x0)) =>
    let P_inO2 :=
      fun x0 : A => inO_leq O1 O2 (P x0) (P_inO1 x0)
      in
    ?Goal) P P_inO1 x)
O1, O2, O3: ReflectiveSubuniverse
H: O1 <=> O2
H0: O2 << O3
H1: O2 <<< O3
Hstrong:= O_strong_leq_trans_l O1 O2 O3: O1 << O3
A: Type
P: A -> Type
P_inO1: forall x : A, In O1 (P x)
P_inO2:= fun x : A => inO_leq O1 O2 (P x) (P_inO1 x): forall x : A, In O2 (P x)
forall x : A,
(fun (P : A -> Type)
   (P_inO1 : forall x0 : A, In O1 (P x0)) =>
 let P_inO2 :=
   fun x0 : A => inO_leq O1 O2 (P x0) (P_inO1 x0) in
 ?Goal) P P_inO1 (to O3 A x) <~> 
P x
  -
O1, O2, O3: ReflectiveSubuniverse
H: O1 <=> O2
H0: O2 << O3
H1: O2 <<< O3
Hstrong:= O_strong_leq_trans_l O1 O2 O3: O1 << O3
A: Type
P: A -> Type
P_inO1: forall x : A, In O1 (P x)
P_inO2:= fun x : A => inO_leq O1 O2 (P x) (P_inO1 x): forall x : A, In O2 (P x)
O_reflector O3 A -> Type exact (OO_descend O3 O2 P).
  -
O1, O2, O3: ReflectiveSubuniverse
H: O1 <=> O2
H0: O2 << O3
H1: O2 <<< O3
Hstrong:= O_strong_leq_trans_l O1 O2 O3: O1 << O3
A: Type
P: A -> Type
P_inO1: forall x : A, In O1 (P x)
P_inO2:= fun x : A => inO_leq O1 O2 (P x) (P_inO1 x): forall x : A, In O2 (P x)
forall x : O_reflector O3 A,
In O1
  ((fun (P : A -> Type)
      (P_inO1 : forall x0 : A, In O1 (P x0)) =>
    let P_inO2 :=
      fun x0 : A => inO_leq O1 O2 (P x0) (P_inO1 x0)
      in
    OO_descend O3 O2 P) P P_inO1 x) intros x; apply (inO_leq O2 O1), (OO_descend_inO O3 O2 P).
  -
O1, O2, O3: ReflectiveSubuniverse
H: O1 <=> O2
H0: O2 << O3
H1: O2 <<< O3
Hstrong:= O_strong_leq_trans_l O1 O2 O3: O1 << O3
A: Type
P: A -> Type
P_inO1: forall x : A, In O1 (P x)
P_inO2:= fun x : A => inO_leq O1 O2 (P x) (P_inO1 x): forall x : A, In O2 (P x)
forall x : A,
(fun (P : A -> Type)
   (P_inO1 : forall x0 : A, In O1 (P x0)) =>
 let P_inO2 :=
   fun x0 : A => inO_leq O1 O2 (P x0) (P_inO1 x0) in
 OO_descend O3 O2 P) P P_inO1 (to O3 A x) <~> P x exact (OO_descend_beta O3 O2 P).
Defined.

(** ** Left exactness properties *)

(** We prove analogues of the properties in section 2.4 of CORS and Theorem 3.1 of RSS, but in a different order, with different proofs, to increase the generality.  The proofs in CORS use Proposition 2.26 for everything else, but it seems that most of the other results are true in the generality of two reflective subuniverses with [O <<< O'], so we give different proofs for some of them.  (To show that this generality is non-spurious, note that a lex modality [O] satisfies [O <<< O], but does not generally coincide with [Sep O].)

In the case of a single modality, most of these statements are equivalent to lex-ness (as stated in Theorem 3.1 of RSS).  We do not know if anything similar is true more generally. *)

Section LeftExactness.
Universe i.
Context (O' O : ReflectiveSubuniverse@{i}) `{O << O', O <<< O'}.

(** Proposition 2.30 of CORS and Theorem 3.1(xii) of RSS: any [O']-equivalence is [O]-connected.  The special case when [f = to O' A] requires only [O << O'], but the general case seems to require [O <<< O']. It is convenient to have this as an instance in this file, but we don't make it global, as it requires that Coq guess [O']. *)
Local Instance conn_map_OO_inverts
       {A B : Type} (f : A -> B) `{O_inverts O' f}
  : IsConnMap O f.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
IsConnMap O f
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
IsConnMap O f
  apply conn_map_from_extension_elim.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
forall P : B -> Type,
(forall b : B, In O (P b)) ->
forall d : forall a : A, P (f a), ExtensionAlong f P d
  intros P P_inO.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
forall d : forall a : A, P (f a), ExtensionAlong f P d
  assert (E : ExtendableAlong 1%nat f P); [ | exact (fst E) ].
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
ExtendableAlong 1 f P
  assert (Qp := OO_descend_beta O' O P).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
Qp: forall x : B,
OO_descend O' O P (to O' B x) <~> P x
ExtendableAlong 1 f P
  assert (Q_inO := OO_descend_inO O' O P).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
Qp: forall x : B,
OO_descend O' O P (to O' B x) <~> P x
Q_inO: forall x : O_reflector O' B,
In O (OO_descend O' O P x)
ExtendableAlong 1 f P
  set (Q := OO_descend O' O P) in *.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
Q:= OO_descend O' O P: O_reflector O' B -> Type
Qp: forall x : B, Q (to O' B x) <~> P x
Q_inO: forall x : O_reflector O' B, In O (Q x)
ExtendableAlong 1 f P
  refine (extendable_postcompose' _ (Q o to O' B) P f Qp _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
Q:= OO_descend O' O P: O_reflector O' B -> Type
Qp: forall x : B, Q (to O' B x) <~> P x
Q_inO: forall x : O_reflector O' B, In O (Q x)
ExtendableAlong 1 f (fun x : B => Q (to O' B x))
  refine (cancelL_extendable _ Q f (to O' B) _ _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
Q:= OO_descend O' O P: O_reflector O' B -> Type
Qp: forall x : B, Q (to O' B x) <~> P x
Q_inO: forall x : O_reflector O' B, In O (Q x)
ExtendableAlong 1 (to O' B) Q
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
Q:= OO_descend O' O P: O_reflector O' B -> Type
Qp: forall x : B, Q (to O' B x) <~> P x
Q_inO: forall x : O_reflector O' B, In O (Q x)
ExtendableAlong 1 (fun x : A => to O' B (f x)) Q
  1:srapply (extendable_conn_map_inO O).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
Q:= OO_descend O' O P: O_reflector O' B -> Type
Qp: forall x : B, Q (to O' B x) <~> P x
Q_inO: forall x : O_reflector O' B, In O (Q x)
ExtendableAlong 1 (fun x : A => to O' B (f x)) Q
  refine (extendable_homotopic _ _ (O_functor O' f o to O' A) (to_O_natural O' f) _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
Q:= OO_descend O' O P: O_reflector O' B -> Type
Qp: forall x : B, Q (to O' B x) <~> P x
Q_inO: forall x : O_reflector O' B, In O (Q x)
ExtendableAlong 1
  (fun x : A => O_functor O' f (to O' A x)) Q
  srapply extendable_compose.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
Q:= OO_descend O' O P: O_reflector O' B -> Type
Qp: forall x : B, Q (to O' B x) <~> P x
Q_inO: forall x : O_reflector O' B, In O (Q x)
ExtendableAlong 1 (O_functor O' f) Q
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
Q:= OO_descend O' O P: O_reflector O' B -> Type
Qp: forall x : B, Q (to O' B x) <~> P x
Q_inO: forall x : O_reflector O' B, In O (Q x)
ExtendableAlong 1 (to O' A)
  (fun b : O_reflector O' A => Q (O_functor O' f b))
  1:srapply extendable_equiv.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: B -> Type
P_inO: forall b : B, In O (P b)
Q:= OO_descend O' O P: O_reflector O' B -> Type
Qp: forall x : B, Q (to O' B x) <~> P x
Q_inO: forall x : O_reflector O' B, In O (Q x)
ExtendableAlong 1 (to O' A)
  (fun b : O_reflector O' A => Q (O_functor O' f b))
  srapply (extendable_conn_map_inO O).
Defined.

(** A generalization of Lemma 2.27 of CORS: [functor_sigma] of a family of [O]-equivalences over an [O']-equivalence is an [O]-equivalence.  CORS Lemma 2.27 is the case when [f = to O' A] and [g] is a family of identities. *)
Definition OO_inverts_functor_sigma 
       {A B : Type} {P : A -> Type} {Q : B -> Type}
       (f : A -> B) (g : forall a, P a -> Q (f a))
       `{O_inverts O' f} `{forall a, O_inverts O (g a)}
  : O_inverts O (functor_sigma f g).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
O_inverts0: O_inverts O' f
H1: forall a : A, O_inverts O (g a)
O_inverts O (functor_sigma f g)
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
O_inverts0: O_inverts O' f
H1: forall a : A, O_inverts O (g a)
O_inverts O (functor_sigma f g)
  srapply isequiv_homotopic'.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
O_inverts0: O_inverts O' f
H1: forall a : A, O_inverts O (g a)
O {x : _ & P x} <~> O {x : _ & Q x}
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
O_inverts0: O_inverts O' f
H1: forall a : A, O_inverts O (g a)
?f == O_functor O (functor_sigma f g)
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
O_inverts0: O_inverts O' f
H1: forall a : A, O_inverts O (g a)
O {x : _ & P x} <~> O {x : _ & Q x} refine (equiv_O_sigma_O O _ oE _ oE (equiv_O_sigma_O O _)^-1).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
O_inverts0: O_inverts O' f
H1: forall a : A, O_inverts O (g a)
O {x : A & O (P x)} <~> O {x : B & O (Q x)}
    exact (Build_Equiv _ _ (O_functor O (functor_sigma f (fun x => O_functor O (g x)))) _).
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
O_inverts0: O_inverts O' f
H1: forall a : A, O_inverts O (g a)
equiv_O_sigma_O O Q
oE {|
     equiv_fun :=
       O_functor O
         (functor_sigma f
            (fun x : A => O_functor O (g x)));
     equiv_isequiv :=
       O_inverts_conn_map O
         (functor_sigma f
            (fun x : A => O_functor O (g x)))
   |} oE (equiv_O_sigma_O O P)^-1 ==
O_functor O (functor_sigma f g) apply O_indpaths.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
O_inverts0: O_inverts O' f
H1: forall a : A, O_inverts O (g a)
(fun x : {x : _ & P x} =>
 (equiv_O_sigma_O O Q
  oE {|
       equiv_fun :=
         O_functor O
           (functor_sigma f
              (fun x0 : A => O_functor O (g x0)));
       equiv_isequiv :=
         O_inverts_conn_map O
           (functor_sigma f
              (fun x0 : A => O_functor O (g x0)))
     |} oE (equiv_O_sigma_O O P)^-1)
   (to O {x : _ & P x} x)) ==
(fun x : {x : _ & P x} =>
 O_functor O (functor_sigma f g)
   (to O {x : _ & P x} x)) intros [x u]; cbn.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
O_inverts0: O_inverts O' f
H1: forall a : A, O_inverts O (g a)
x: A
u: P x
O_rec
  (fun X : {x : B & O (Q x)} =>
   O_rec
     (fun p : Q X.1 => to O {x : B & Q x} (X.1; p))
     X.2)
  (O_functor O
     (functor_sigma f (fun x : A => O_functor O (g x)))
     (O_functor O
        (functor_sigma idmap (fun x : A => to O (P x)))
        (to O {x : _ & P x} (x; u)))) =
O_functor O (functor_sigma f g)
  (to O {x : _ & P x} (x; u))
    rewrite !to_O_natural, O_rec_beta; cbn.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
O_inverts0: O_inverts O' f
H1: forall a : A, O_inverts O (g a)
x: A
u: P x
O_rec (fun p : Q (f x) => to O {x : B & Q x} (f x; p))
  (O_functor O (g x) (to O (P x) u)) =
to O {x : _ & Q x} (functor_sigma f g (x; u))
    rewrite !to_O_natural, O_rec_beta.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
P: A -> Type
Q: B -> Type
f: A -> B
g: forall a : A, P a -> Q (f a)
O_inverts0: O_inverts O' f
H1: forall a : A, O_inverts O (g a)
x: A
u: P x
to O {x : B & Q x} (f x; g x u) =
to O {x : _ & Q x} (functor_sigma f g (x; u))
    reflexivity.
Defined.

(** Families of [O]-modal types descend along all [O']-equivalences (not just the [O']-units, as asserted in the definition of [<<<]. *)
Definition OO_descend_O_inverts
           {A B : Type} (f : A -> B) `{O_inverts O' f}
           (P : A -> Type) {P_inO : forall x, In O (P x)}
  : B -> Type.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type
P_inO: forall x : A, In O (P x)
B -> Type
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type
P_inO: forall x : A, In O (P x)
B -> Type
  intros b.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type
P_inO: forall x : A, In O (P x)
b: B
Type
  pose (Q := OO_descend O' O P).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type
P_inO: forall x : A, In O (P x)
b: B
Q:= OO_descend O' O P: O_reflector O' A -> Type
Type
  exact (Q ((O_functor O' f)^-1 (to O' B b))).
Defined.

#[export] Instance OO_descend_O_inverts_inO
       {A B : Type} (f : A -> B) `{O_inverts O' f}
       (P : A -> Type) {P_inO : forall x, In O (P x)} (b : B)
  : In O (OO_descend_O_inverts f P b)
  := _.

Definition OO_descend_O_inverts_beta
           {A B : Type} (f : A -> B) `{O_inverts O' f}
           (P : A -> Type) {P_inO : forall x, In O (P x)} (a : A)
  : (OO_descend_O_inverts f P (f a)) <~> P a.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type
P_inO: forall x : A, In O (P x)
a: A
OO_descend_O_inverts f P (f a) <~> P a
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type
P_inO: forall x : A, In O (P x)
a: A
OO_descend_O_inverts f P (f a) <~> P a
  unfold OO_descend_O_inverts.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type
P_inO: forall x : A, In O (P x)
a: A
OO_descend O' O P
  ((O_functor O' f)^-1 (to O' B (f a))) <~> P a
  refine (OO_descend_beta O' O P a oE _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type
P_inO: forall x : A, In O (P x)
a: A
OO_descend O' O P
  ((O_functor O' f)^-1 (to O' B (f a))) <~>
OO_descend O' O P (to O' A a)
  assert (p := (to_O_natural O' f a)^).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type
P_inO: forall x : A, In O (P x)
a: A
p: to O' B (f a) = O_functor O' f (to O' A a)
OO_descend O' O P
  ((O_functor O' f)^-1 (to O' B (f a))) <~>
OO_descend O' O P (to O' A a)
  apply moveR_equiv_V in p.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type
P_inO: forall x : A, In O (P x)
a: A
p: (O_functor O' f)^-1 (to O' B (f a)) = to O' A a
OO_descend O' O P
  ((O_functor O' f)^-1 (to O' B (f a))) <~>
OO_descend O' O P (to O' A a)
  exact (equiv_transport _ p).
Defined.

(** Morally, an equivalent way of saying [O <<< O'] is that the universe of [O]-modal types is [O']-modal.  We can't say this directly since this type lives in a higher universe, but here is a rephrasing of it. *)
Definition ooextendable_TypeO_lex_leq `{Univalence}
           {A B : Type} (f : A -> B) `{O_inverts O' f}
  : ooExtendableAlong f (fun _ => Type_ O).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: Univalence
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
ooExtendableAlong f (fun _ : B => Type_ O)
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: Univalence
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
ooExtendableAlong f (fun _ : B => Type_ O)
  rapply ooextendable_TypeO_from_extension; intros P.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: Univalence
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type_ O
ExtensionAlong f (fun _ : B => Type_ O) P
  exists (fun x => (OO_descend_O_inverts f P x ;
                    OO_descend_O_inverts_inO f P x)).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: Univalence
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type_ O
forall x : A,
(OO_descend_O_inverts f (fun x0 : A => P x0) (f x);
OO_descend_O_inverts_inO f (fun x0 : A => P x0) (f x)) =
P x
  intros x; apply path_TypeO, path_universe_uncurried; cbn.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: Univalence
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
P: A -> Type_ O
x: A
OO_descend_O_inverts f (fun x : A => P x) (f x) <~>
(P x).1
  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). *)
#[export] Instance inO_TypeO_lex_leq `{Univalence} `{IsAccRSU O'}
  : In (lift_accrsu O') (Type_ O)
  := fun i => ooextendable_TypeO_lex_leq (acc_lgen O' i).

(** If [f] is an [O']-equivalence, then [ap f] is an [O]-equivalence. *)
#[export] Instance OO_inverts_ap@{}
       {A B : Type@{i}} (f : A -> B) `{O_inverts O' f} (x y : A)
  : O_inverts O (@ap _ _ f x y).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
O_inverts O (ap f)
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
O_inverts O (ap f)
  assert (Pb := OO_descend_O_inverts_beta f (fun y:A => O (x = y))).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
Pb: forall a : A,
OO_descend_O_inverts f 
  (fun y : A => O (x = y)) 
  (f a) <~> (fun y : A => O (x = y)) a
O_inverts O (ap f)
  assert (P_inO := OO_descend_O_inverts_inO f (fun y:A => O (x = y))).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
Pb: forall a : A,
OO_descend_O_inverts f 
  (fun y : A => O (x = y)) 
  (f a) <~> (fun y : A => O (x = y)) a
P_inO: forall b : B,
In O
  (OO_descend_O_inverts f
     (fun y : A => O (x = y)) b)
O_inverts O (ap f)
  set (P := OO_descend_O_inverts f (fun y:A => O (x = y))) in *.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P:= OO_descend_O_inverts f (fun y : A => O (x = y)): B -> Type
Pb: forall a : A,
P (f a) <~> (fun y : A => O (x = y)) a
P_inO: forall b : B, In O (P b)
O_inverts O (ap f)
  clearbody P; cbn in *.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
O_inverts O (ap f)
  srapply isequiv_adjointify.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
O (f x = f y) -> O (x = y)
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
O_functor O (ap f) o ?g == idmap
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
?g o O_functor O (ap f) == idmap
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
O (f x = f y) -> O (x = y) intros q.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
q: O (f x = f y)
O (x = y)
    pose (t := fun p => @transport B P (f x) (f y) p ((Pb x)^-1 (to O (x = x) 1))).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
q: O (f x = f y)
t:= fun p : f x = f y =>
transport P p ((Pb x)^-1 (to O (x = x) 1)): f x = f y -> P (f y)
O (x = y)
    exact (Pb y (O_rec t q)).
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
O_functor O (ap f)
o (fun q : O (f x = f y) =>
   let t :=
     fun p : f x = f y =>
     transport P p ((Pb x)^-1 (to O (x = x) 1)) in
   Pb y (O_rec t q)) == idmap apply O_indpaths; intros p; cbn.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
O_functor O (ap f)
  (Pb y
     (O_rec
        (fun p : f x = f y =>
         transport P p ((Pb x)^-1 (to O (x = x) 1)))
        (to O (f x = f y) p))) = to O (f x = f y) p
    rewrite O_rec_beta.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
O_functor O (ap f)
  (Pb y (transport P p ((Pb x)^-1 (to O (x = x) 1)))) =
to O (f x = f y) p
    assert (g := extension_conn_map_elim O (functor_sigma f (fun (a:A) (p:P (f a)) => p))
                                         (fun bp => O (f x = bp.1)) (fun u => O_functor O (ap f) (Pb u.1 u.2))).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
O_functor O (ap f)
  (Pb y (transport P p ((Pb x)^-1 (to O (x = x) 1)))) =
to O (f x = f y) p 
    pose (g1 b p := g.1 (b;p)).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall (b : B) (p : P b),
(fun bp : {x : _ & P x} => O (f x = bp.1)) (b; p)
O_functor O (ap f)
  (Pb y (transport P p ((Pb x)^-1 (to O (x = x) 1)))) =
to O (f x = f y) p cbn in g1.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall b : B, P b -> O (f x = b)
O_functor O (ap f)
  (Pb y (transport P p ((Pb x)^-1 (to O (x = x) 1)))) =
to O (f x = f y) p
    assert (e : (fun u => g1 u.1 u.2) == g.1).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall b : B, P b -> O (f x = b)
(fun u : {x : _ & P x} => g1 u.1 u.2) == g.1
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall b : B, P b -> O (f x = b)
e: (fun u : {x : _ & P x} => g1 u.1 u.2) == g.1
O_functor O (ap f)
  (Pb y (transport P p ((Pb x)^-1 (to O (x = x) 1)))) =
to O (f x = f y) p 
    1:intros [a b]; reflexivity.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall b : B, P b -> O (f x = b)
e: (fun u : {x : _ & P x} => g1 u.1 u.2) == g.1
O_functor O (ap f)
  (Pb y (transport P p ((Pb x)^-1 (to O (x = x) 1)))) =
to O (f x = f y) p
    assert (g2 := fun a p => e _ @ g.2 (a;p)); cbn in g2.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall b : B, P b -> O (f x = b)
e: (fun u : {x : _ & P x} => g1 u.1 u.2) == g.1
g2: forall (a : A) (p : P (f a)),
g1 (f a) p = O_functor O (ap f) (Pb a p)
O_functor O (ap f)
  (Pb y (transport P p ((Pb x)^-1 (to O (x = x) 1)))) =
to O (f x = f y) p
    refine ((g2 y _)^ @ _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall b : B, P b -> O (f x = b)
e: (fun u : {x : _ & P x} => g1 u.1 u.2) == g.1
g2: forall (a : A) (p : P (f a)),
g1 (f a) p = O_functor O (ap f) (Pb a p)
g1 (f y) (transport P p ((Pb x)^-1 (to O (x = x) 1))) =
to O (f x = f y) p
    rewrite (ap_transport p g1).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall b : B, P b -> O (f x = b)
e: (fun u : {x : _ & P x} => g1 u.1 u.2) == g.1
g2: forall (a : A) (p : P (f a)),
g1 (f a) p = O_functor O (ap f) (Pb a p)
transport (fun b : B => O (f x = b)) p
  (g1 (f x) ((Pb x)^-1 (to O (x = x) 1))) =
to O (f x = f y) p
    rewrite (g2 x ((Pb x)^-1 (to O (x = x) 1))).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall b : B, P b -> O (f x = b)
e: (fun u : {x : _ & P x} => g1 u.1 u.2) == g.1
g2: forall (a : A) (p : P (f a)),
g1 (f a) p = O_functor O (ap f) (Pb a p)
transport (fun b : B => O (f x = b)) p
  (O_functor O (ap f)
     (Pb x ((Pb x)^-1 (to O (x = x) 1)))) =
to O (f x = f y) p
    rewrite eisretr, to_O_natural; cbn.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall b : B, P b -> O (f x = b)
e: (fun u : {x : _ & P x} => g1 u.1 u.2) == g.1
g2: forall (a : A) (p : P (f a)),
g1 (f a) p = O_functor O (ap f) (Pb a p)
transport (fun b : B => O (f x = b)) p
  (to O (f x = f x) 1) = to O (f x = f y) p
    rewrite <- (ap_transport p (fun b => to O (f x = b))).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall b : B, P b -> O (f x = b)
e: (fun u : {x : _ & P x} => g1 u.1 u.2) == g.1
g2: forall (a : A) (p : P (f a)),
g1 (f a) p = O_functor O (ap f) (Pb a p)
to O (f x = f y) (transport (paths (f x)) p 1) =
to O (f x = f y) p
    apply ap.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall b : B, P b -> O (f x = b)
e: (fun u : {x : _ & P x} => g1 u.1 u.2) == g.1
g2: forall (a : A) (p : P (f a)),
g1 (f a) p = O_functor O (ap f) (Pb a p)
transport (paths (f x)) p 1 = p
    rewrite transport_paths_r.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: f x = f y
g: ExtensionAlong
  (functor_sigma f (fun a : A => idmap))
  (fun bp : {x : _ & P x} => O (f x = bp.1))
  (fun u : {a : A & P (f a)} =>
   O_functor O (ap f) (Pb u.1 u.2))
g1:= fun (b : B) (p : P b) => g.1 (b; p): forall b : B, P b -> O (f x = b)
e: (fun u : {x : _ & P x} => g1 u.1 u.2) == g.1
g2: forall (a : A) (p : P (f a)),
g1 (f a) p = O_functor O (ap f) (Pb a p)
1 @ p = p
    apply concat_1p.
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
(fun q : O (f x = f y) =>
 let t :=
   fun p : f x = f y =>
   transport P p ((Pb x)^-1 (to O (x = x) 1)) in
 Pb y (O_rec t q)) o O_functor O (ap f) == idmap apply O_indpaths; intros p; cbn.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: x = y
Pb y
  (O_rec
     (fun p : f x = f y =>
      transport P p ((Pb x)^-1 (to O (x = x) 1)))
     (O_functor O (ap f) (to O (x = y) p))) =
to O (x = y) p
    rewrite to_O_natural, O_rec_beta.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x, y: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
p: x = y
Pb y
  (transport P (ap f p) ((Pb x)^-1 (to O (x = x) 1))) =
to O (x = y) p
    destruct p; cbn.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B: Type
f: A -> B
O_inverts0: O_inverts O' f
x: A
P: B -> Type
Pb: forall a : A, P (f a) <~> O (x = a)
P_inO: forall b : B, In O (P b)
Pb x (transport P 1 ((Pb x)^-1 (to O (x = x) 1))) =
to O (x = x) 1
    srapply eisretr.
Defined.

Definition equiv_O_functor_ap_OO_inverts
       {A B : Type} (f : A -> B) `{O_inverts O' f} (x y : A)
  : O (x = y) <~> O (f x = f y)
  := Build_Equiv _ _ (O_functor O (ap f)) _.

(** Theorem 3.1(i) of RSS: path-spaces of [O']-connected types are [O]-connected. *)
Definition OO_isconnected_paths
           {A : Type} `{IsConnected O' A} (x y : A)
  : IsConnected O (x = y).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A: Type
H1: IsConnected O' A
x, y: A
IsConnected O (x = y)
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A: Type
H1: IsConnected O' A
x, y: A
IsConnected O (x = y)
  exact (contr_equiv' _ (equiv_O_functor_ap_OO_inverts (const_tt _) x y)^-1).
Defined.

(** Proposition 2.26 of CORS and Theorem 3.1(ix) of RSS; also generalizes Theorem 7.3.12 of the book.  Here we need to add the extra assumption that [O' <= Sep O], which is satisfied when [O' = Sep O] but also when [O] is lex and [O' = O].  That some such extra hypothesis is necessary can be seen from the fact that [Tr (-2) <<< O'] for any [O'], whereas this statement is certainly not true in that generality. *)
Definition path_OO `{O' <= Sep O}
           {X : Type@{i}} (x y : X)
  : O (x = y) -> (to O' X x = to O' X y).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
X: Type
x, y: X
O (x = y) -> to O' X x = to O' X y
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
X: Type
x, y: X
O (x = y) -> to O' X x = to O' X y
  nrefine (O_rec (O := O) (@ap X (O' X) (to O' X) x y)).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
X: Type
x, y: X
In O (to O' X x = to O' X y)
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
X: Type
x, y: X
Reflects O (x = y)
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
X: Type
x, y: X
In O (to O' X x = to O' X y) rapply (@inO_leq O' (Sep O)).
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
X: Type
x, y: X
Reflects O (x = y) exact _.
Defined.

#[export] Instance isequiv_path_OO `{O' <= Sep O}
       {X : Type@{i}} (x y : X)
  : IsEquiv (path_OO x y).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
X: Type
x, y: X
IsEquiv (path_OO x y)
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
X: Type
x, y: X
IsEquiv (path_OO x y)
  nrefine (isequiv_O_rec_O_inverts O _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
X: Type
x, y: X
O_inverts O (ap (to O' X))
  (** Typeclass search can find this, but it's quicker (and may help the reader) to give it explicitly. *)
  apply (OO_inverts_ap (to O' X)).
Defined.

Definition equiv_path_OO `{O' <= Sep O}
           {X : Type@{i}} (x y : X)
  : 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. *)
#[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)
       `{O_inverts O' h, O_inverts O' k}
  : O_inverts O (functor_hfiber p b).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
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
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts O (functor_hfiber p b)
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
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
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts O (functor_hfiber p b)
  unfold functor_hfiber.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
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
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts O
  (functor_sigma h
     (fun (a : A) (e : f a = b) => (p a)^ @ ap k e))
  snrefine (OO_inverts_functor_sigma _ _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
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
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts O' h
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
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
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
forall a : A,
O_inverts O
  ((fun (a0 : A) (e : f a0 = b) => (p a0)^ @ ap k e) a)
  1:exact _.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
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
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
forall a : A,
O_inverts O
  ((fun (a0 : A) (e : f a0 = b) => (p a0)^ @ ap k e) a)
  intros a; cbn.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
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
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
a: A
O_inverts O (fun e : f a = b => (p a)^ @ ap k e)
  refine (isequiv_homotopic (O_functor O (concat (p a)^) o O_functor O (@ap _ _ k (f a) b)) _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
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
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
a: A
(fun x : O (f a = b) =>
 O_functor O (concat (p a)^) (O_functor O (ap k) x)) ==
O_functor O (fun e : f a = b => (p a)^ @ ap k e)
  symmetry; apply O_functor_compose.
Defined.

(** Corollary 2.29 of CORS: [O'] preserves fibers up to [O]-equivalence. *)
#[export] Instance OO_inverts_functor_hfiber_to_O
       {Y X : Type} (f : Y -> X) (x : X)
  : O_inverts O (functor_hfiber (fun a => (to_O_natural O' f a)^) x).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X: Type
f: Y -> X
x: X
O_inverts O
  (functor_hfiber
     (fun a : Y => (to_O_natural O' f a)^) x)
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X: Type
f: Y -> X
x: X
O_inverts O
  (functor_hfiber
     (fun a : Y => (to_O_natural O' f a)^) x)
  (** Typeclass search can find this, but it's faster to give it explicitly. *)
  exact (OO_inverts_functor_hfiber _ _).
Defined.

Definition equiv_OO_functor_hfiber_to_O
           {Y X : Type@{i} } (f : Y -> X) (x : X)
  : 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.) *)
Definition OO_conn_map_isconnected
       {Y X : Type} `{IsConnected O' Y, IsConnected O' X} (f : Y -> X)
  : IsConnMap O f.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X: Type
H1: IsConnected O' Y
H2: IsConnected O' X
f: Y -> X
IsConnMap O f
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X: Type
H1: IsConnected O' Y
H2: IsConnected O' X
f: Y -> X
IsConnMap O f
  intros x; exact (contr_equiv' _ (equiv_OO_functor_hfiber_to_O f x)^-1).
Defined.

Definition OO_isconnected_hfiber
       {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. *)
Definition OO_isequiv_mapino_isconnected
       {Y X : Type} `{IsConnected O' Y, IsConnected O' X} (f : Y -> X) `{MapIn O _ _ f}
  : IsEquiv f.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X: Type
H1: IsConnected O' Y
H2: IsConnected O' X
f: Y -> X
H3: MapIn O f
IsEquiv f
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X: Type
H1: IsConnected O' Y
H2: IsConnected O' X
f: Y -> X
H3: MapIn O f
IsEquiv f
  apply (isequiv_conn_ino_map O).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X: Type
H1: IsConnected O' Y
H2: IsConnected O' X
f: Y -> X
H3: MapIn O f
IsConnMap O f
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X: Type
H1: IsConnected O' Y
H2: IsConnected O' X
f: Y -> X
H3: MapIn O f
MapIn O f
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X: Type
H1: IsConnected O' Y
H2: IsConnected O' X
f: Y -> X
H3: MapIn O f
IsConnMap O f apply OO_conn_map_isconnected.
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X: Type
H1: IsConnected O' Y
H2: IsConnected O' X
f: Y -> X
H3: MapIn O f
MapIn O f assumption.
Defined.

(** Theorem 3.1(vi) of RSS (and 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}
           (p : k o f == g o h) (b : B)
  : IsConnMap O (functor_hfiber p b).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
H1: IsConnMap O' h
H2: IsConnMap O' k
p: k o f == g o h
b: B
IsConnMap O (functor_hfiber p b)
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
H1: IsConnMap O' h
H2: IsConnMap O' k
p: k o f == g o h
b: B
IsConnMap O (functor_hfiber p b)
  intros [c q].
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
H1: IsConnMap O' h
H2: IsConnMap O' k
p: k o f == g o h
b: B
c: C
q: g c = k b
IsConnected O (hfiber (functor_hfiber p b) (c; q))
  nrefine (isconnected_equiv' O _ (hfiber_functor_hfiber p b c q)^-1 _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
H1: IsConnMap O' h
H2: IsConnMap O' k
p: k o f == g o h
b: B
c: C
q: g c = k b
IsConnected O
  (hfiber (functor_hfiber (fun x : A => (p x)^) c)
     (b; q^))
  apply OO_isconnected_hfiber.
Defined.

(** An enhancement of Corollary 2.29 of CORS, corresponding to Theorem 3.1(viii) of RSS: when [O'] is a modality, the map between fibers is not just an O-equivalence but is O-connected. *)
#[export] Instance OO_conn_map_functor_hfiber_to_O `{IsModality O'}
       {Y X : Type} (f : Y -> X) (x : X)
  : IsConnMap O (functor_hfiber (fun y => (to_O_natural O' f y)^) x).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
IsModality0: IsModality O'
Y, X: Type
f: Y -> X
x: X
IsConnMap O
  (functor_hfiber
     (fun y : Y => (to_O_natural O' f y)^) x)
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
IsModality0: IsModality O'
Y, X: Type
f: Y -> X
x: X
IsConnMap O
  (functor_hfiber
     (fun y : Y => (to_O_natural O' f y)^) x)
  apply OO_conn_map_functor_hfiber.
Defined.

(** Theorem 3.1(vii) of RSS *)
Definition OO_ispullback_connmap_mapino
           {A B C D : Type} {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D}
           (p : k o f == g o h)
           `{O_inverts O' h, O_inverts O' k, MapIn O _ _ f, MapIn O _ _ g}
  : IsPullback p.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
H1: MapIn O f
H2: MapIn O g
IsPullback p
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
H1: MapIn O f
H2: MapIn O g
IsPullback p
  apply ispullback_isequiv_functor_hfiber; intros b.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
H1: MapIn O f
H2: MapIn O g
b: B
IsEquiv (functor_hfiber p b)
  apply (isequiv_O_inverts O).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B, C, D: Type
f: A -> B
g: C -> D
h: A -> C
k: B -> D
p: k o f == g o h
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
H1: MapIn O f
H2: MapIn O g
b: B
O_inverts O (functor_hfiber p b)
  apply OO_inverts_functor_hfiber; exact _.
Defined.

(** [functor_pullback] on a triple of [O']-equivalences is an [O]-equivalence. *)
#[export] Instance OO_inverts_functor_pullback
       {A1 B1 C1 A2 B2 C2 : Type}
       (f1 : B1 -> A1) (g1 : C1 -> A1)
       (f2 : B2 -> A2) (g2 : C2 -> A2)
       (h : A1 -> A2) (k : B1 -> B2) (l : C1 -> C2)
       (p : f2 o k == h o f1) (q : g2 o l == h o g1)
       `{O_inverts O' h, O_inverts O' k, O_inverts O' l}
  : O_inverts O (functor_pullback f1 g1 f2 g2 h k l p q).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
O_inverts O (functor_pullback f1 g1 f2 g2 h k l p q)
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
O_inverts O (functor_pullback f1 g1 f2 g2 h k l p q)
  unfold functor_pullback.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
O_inverts O
  (functor_sigma k
     (fun b1 : B1 =>
      functor_sigma l
        (fun (c1 : C1) (e1 : f1 b1 = g1 c1) =>
         (p b1 @ ap h e1) @ (q c1)^)))
  snrefine (OO_inverts_functor_sigma _ _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
O_inverts O' k
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
forall a : B1,
O_inverts O
  ((fun b1 : B1 =>
    functor_sigma l
      (fun (c1 : C1) (e1 : f1 b1 = g1 c1) =>
       (p b1 @ ap h e1) @ (q c1)^)) a)
  1:exact _.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
forall a : B1,
O_inverts O
  ((fun b1 : B1 =>
    functor_sigma l
      (fun (c1 : C1) (e1 : f1 b1 = g1 c1) =>
       (p b1 @ ap h e1) @ (q c1)^)) a)
  intros b1; cbn.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
b1: B1
O_inverts O
  (functor_sigma l
     (fun (c1 : C1) (e1 : f1 b1 = g1 c1) =>
      (p b1 @ ap h e1) @ (q c1)^))
  snrefine (OO_inverts_functor_sigma _ _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
b1: B1
O_inverts O' l
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
b1: B1
forall a : C1,
O_inverts O
  ((fun (c1 : C1) (e1 : f1 b1 = g1 c1) =>
    (p b1 @ ap h e1) @ (q c1)^) a)
  1:exact _.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
b1: B1
forall a : C1,
O_inverts O
  ((fun (c1 : C1) (e1 : f1 b1 = g1 c1) =>
    (p b1 @ ap h e1) @ (q c1)^) a)
  intros c1; cbn.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
b1: B1
c1: C1
O_inverts O
  (fun e1 : f1 b1 = g1 c1 =>
   (p b1 @ ap h e1) @ (q c1)^)
  pose @isequiv_compose. (* Speed up typeclass search. *)
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
b1: B1
c1: C1
i:= @isequiv_compose: forall (A B C : Type) 
(f : A -> B),
IsEquiv f ->
forall g : B -> C, IsEquiv g -> IsEquiv (g o f)
O_inverts O
  (fun e1 : f1 b1 = g1 c1 =>
   (p b1 @ ap h e1) @ (q c1)^)
  refine (isequiv_homotopic (O_functor O (fun r => r @ (q c1)^) o O_functor O (concat (p b1)) o O_functor O (@ap _ _ h (f1 b1) (g1 c1))) _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
b1: B1
c1: C1
i:= @isequiv_compose: forall (A B C : Type) 
(f : A -> B),
IsEquiv f ->
forall g : B -> C, IsEquiv g -> IsEquiv (g o f)
(fun x : O (f1 b1 = g1 c1) =>
 O_functor O
   (fun r : f2 (k b1) = h (g1 c1) => r @ (q c1)^)
   (O_functor O (concat (p b1)) (O_functor O (ap h) x))) ==
O_functor O
  (fun e1 : f1 b1 = g1 c1 =>
   (p b1 @ ap h e1) @ (q c1)^)
  intros r; symmetry.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
b1: B1
c1: C1
i:= @isequiv_compose: forall (A B C : Type) 
(f : A -> B),
IsEquiv f ->
forall g : B -> C, IsEquiv g -> IsEquiv (g o f)
r: O (f1 b1 = g1 c1)
O_functor O
  (fun e1 : f1 b1 = g1 c1 =>
   (p b1 @ ap h e1) @ (q c1)^) r =
O_functor O
  (fun r : f2 (k b1) = h (g1 c1) => r @ (q c1)^)
  (O_functor O (concat (p b1)) (O_functor O (ap h) r)) 
  refine (_ @ _).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
b1: B1
c1: C1
i:= @isequiv_compose: forall (A B C : Type) 
(f : A -> B),
IsEquiv f ->
forall g : B -> C, IsEquiv g -> IsEquiv (g o f)
r: O (f1 b1 = g1 c1)
O_functor O
  (fun e1 : f1 b1 = g1 c1 =>
   (p b1 @ ap h e1) @ (q c1)^) r = ?Goal
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
b1: B1
c1: C1
i:= @isequiv_compose: forall (A B C : Type) 
(f : A -> B),
IsEquiv f ->
forall g : B -> C, IsEquiv g -> IsEquiv (g o f)
r: O (f1 b1 = g1 c1)
?Goal =
O_functor O
  (fun r : f2 (k b1) = h (g1 c1) => r @ (q c1)^)
  (O_functor O (concat (p b1)) (O_functor O (ap h) r))
  2:apply O_functor_compose.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A1, B1, C1, A2, B2, C2: Type
f1: B1 -> A1
g1: C1 -> A1
f2: B2 -> A2
g2: C2 -> A2
h: A1 -> A2
k: B1 -> B2
l: C1 -> C2
p: f2 o k == h o f1
q: g2 o l == h o g1
O_inverts0: O_inverts O' h
O_inverts1: O_inverts O' k
O_inverts2: O_inverts O' l
b1: B1
c1: C1
i:= @isequiv_compose: forall (A B C : Type) 
(f : A -> B),
IsEquiv f ->
forall g : B -> C, IsEquiv g -> IsEquiv (g o f)
r: O (f1 b1 = g1 c1)
O_functor O
  (fun e1 : f1 b1 = g1 c1 =>
   (p b1 @ ap h e1) @ (q c1)^) r =
O_functor O
  (fun x : h (f1 b1) = h (g1 c1) =>
   (fun r : f2 (k b1) = h (g1 c1) => r @ (q c1)^)
     (p b1 @ x)) (O_functor O (ap h) r)
  cbn; srapply O_functor_compose.
Defined.

(** Proposition 2.28 of CORS, and Theorem 3.1(x) of RSS: the functor [O'] preserves pullbacks up to [O]-equivalence. *)
#[export] Instance OO_inverts_functor_pullback_to_O
       {A B C : Type} (f : B -> A) (g : C -> A)
  : O_inverts O (functor_pullback f g (O_functor O' f) (O_functor O' g)
                                  (to O' A) (to O' B) (to O' C)
                                  (to_O_natural O' f) (to_O_natural O' g)).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B, C: Type
f: B -> A
g: C -> A
O_inverts O
  (functor_pullback f g (O_functor O' f)
     (O_functor O' g) (to O' A) (to O' B) (to O' C)
     (to_O_natural O' f) (to_O_natural O' g))
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
A, B, C: Type
f: B -> A
g: C -> A
O_inverts O
  (functor_pullback f g (O_functor O' f)
     (O_functor O' g) (to O' A) (to O' B) (to O' C)
     (to_O_natural O' f) (to_O_natural O' g))
  apply OO_inverts_functor_pullback; exact _.
Defined.

Definition equiv_OO_pullback {A B C : Type} (f : B -> A) (g : C -> A)
  : O (Pullback f g) <~> O (Pullback (O_functor O' f) (O_functor O' g))
  := Build_Equiv _ _ _ (OO_inverts_functor_pullback_to_O f g).

(** The "if" direction of CORS Proposition 2.31, and the nontrivial part of Theorem 3.1(xi) of RSS.  Note that we could also deduce Theorem 3.1(iii) of RSS from this. *)
Definition OO_cancelL_conn_map
           {Y X Z : Type} (f : Y -> X) (g : X -> Z)
           `{IsConnMap O' _ _ (g o f)} `{IsConnMap O' _ _ g}
  : IsConnMap O f.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O' g
IsConnMap O f
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O' g
IsConnMap O f
  apply conn_map_OO_inverts.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O' g
O_inverts O' f
  napply (cancelL_isequiv (O_functor O' g)).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O' g
O_inverts O' g
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O' g
IsEquiv
  (fun x : O' Y => O_functor O' g (O_functor O' f x))
  1:exact _.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O' g
IsEquiv
  (fun x : O' Y => O_functor O' g (O_functor O' f x))
  exact (isequiv_homotopic _ (O_functor_compose O' f g)).
Defined.

End LeftExactness.

(** Here's the "only if" direction of CORS Proposition 2.31.  Note that the hypotheses are different from those of the "if" direction, and the proof is shorter than the one given in CORS. *)
Definition OO_cancelR_conn_map
       (O' O : ReflectiveSubuniverse@{u}) `{O_leq@{u u u} O O', O' <= Sep O}
       {Y X Z : Type} (f : Y -> X) (g : X -> Z)
       `{IsConnMap O' _ _ (g o f)} `{IsConnMap O _ _ f}
  : IsConnMap O' g.
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O f
IsConnMap O' g
Proof.
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O f
IsConnMap O' g
  apply conn_map_from_extension_elim.
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O f
forall P : Z -> Type,
(forall b : Z, In O' (P b)) ->
forall d : forall a : X, P (g a), ExtensionAlong g P d
  intros P P_inO h.
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O f
P: Z -> Type
P_inO: forall b : Z, In O' (P b)
h: forall a : X, P (g a)
ExtensionAlong g P h
  exists (conn_map_elim O' (g o f) P (h o f)).
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O f
P: Z -> Type
P_inO: forall b : Z, In O' (P b)
h: forall a : X, P (g a)
forall x : X,
conn_map_elim O' (fun x0 : Y => g (f x0)) P
  (fun x0 : Y => h (f x0)) 
  (g x) = h x
  nrefine (conn_map_elim O f _ _); [ exact _ | .. ].
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O f
P: Z -> Type
P_inO: forall b : Z, In O' (P b)
h: forall a : X, P (g a)
forall b : X,
In O
  (conn_map_elim O' (fun x : Y => g (f x)) P
     (fun x : Y => h (f x)) 
     (g b) = h b)
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O f
P: Z -> Type
P_inO: forall b : Z, In O' (P b)
h: forall a : X, P (g a)
forall a : Y,
conn_map_elim O' (fun x : Y => g (f x)) P
  (fun x : Y => h (f x)) 
  (g (f a)) = h (f a)
  -
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O f
P: Z -> Type
P_inO: forall b : Z, In O' (P b)
h: forall a : X, P (g a)
forall b : X,
In O
  (conn_map_elim O' (fun x : Y => g (f x)) P
     (fun x : Y => h (f x)) 
     (g b) = h b) intros x.
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O f
P: Z -> Type
P_inO: forall b : Z, In O' (P b)
h: forall a : X, P (g a)
x: X
In O
  (conn_map_elim O' (fun x : Y => g (f x)) P
     (fun x : Y => h (f x)) 
     (g x) = h x)
    pose proof (fun z => inO_leq O' (Sep O) (P z) (P_inO z)).
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O f
P: Z -> Type
P_inO: forall b : Z, In O' (P b)
h: forall a : X, P (g a)
x: X
X0: forall z : Z, In (Sep O) (P z)
In O
  (conn_map_elim O' (fun x : Y => g (f x)) P
     (fun x : Y => h (f x)) 
     (g x) = h x)
    exact _.
  -
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O f
P: Z -> Type
P_inO: forall b : Z, In O' (P b)
h: forall a : X, P (g a)
forall a : Y,
conn_map_elim O' (fun x : Y => g (f x)) P
  (fun x : Y => h (f x)) 
  (g (f a)) = h (f a) intros y.
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H1: IsConnMap O' (g o f)
H2: IsConnMap O f
P: Z -> Type
P_inO: forall b : Z, In O' (P b)
h: forall a : X, P (g a)
y: Y
conn_map_elim O' (fun x : Y => g (f x)) P
  (fun x : Y => h (f x)) 
  (g (f y)) = h (f y)
    apply (conn_map_comp O' (g o f)).
Defined.

Definition OO_isconnected_from_conn_map
       (O' O : ReflectiveSubuniverse) `{O <= O', O' <= Sep O}
       {Y X : Type} (f : Y -> X)
       `{IsConnected O' Y} `{IsConnMap O _ _ f}
  : IsConnected O' X.
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X: Type
f: Y -> X
H1: IsConnected O' Y
H2: IsConnMap O f
IsConnected O' X
Proof.
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X: Type
f: Y -> X
H1: IsConnected O' Y
H2: IsConnMap O f
IsConnected O' X
  apply isconnected_conn_map_to_unit.
O', O: ReflectiveSubuniverse
H: O <= O'
H0: O' <= Sep O
Y, X: Type
f: Y -> X
H1: IsConnected O' Y
H2: IsConnMap O f
IsConnMap O' (const_tt X)
  exact (OO_cancelR_conn_map O' O f (const_tt _)).
Defined.

(** An interesting scholium to Proposition 2.31. *)
Definition OO_inverts_conn_map_factor_conn_map
       (O' O : ReflectiveSubuniverse) `{O << O', O <<< O', O' <= Sep O}
       {Y X Z : Type} (f : Y -> X) (g : X -> Z)
       `{IsConnMap O' _ _ (g o f)} `{IsConnMap O _ _ f}
  : O_inverts O' f.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H2: IsConnMap O' (g o f)
H3: IsConnMap O f
O_inverts O' f
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H2: IsConnMap O' (g o f)
H3: IsConnMap O f
O_inverts O' f
  napply (cancelL_isequiv (O_functor O' g)).
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H2: IsConnMap O' (g o f)
H3: IsConnMap O f
O_inverts O' g
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H2: IsConnMap O' (g o f)
H3: IsConnMap O f
IsEquiv
  (fun x : O' Y => O_functor O' g (O_functor O' f x))
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H2: IsConnMap O' (g o f)
H3: IsConnMap O f
O_inverts O' g apply O_inverts_conn_map.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H2: IsConnMap O' (g o f)
H3: IsConnMap O f
IsConnMap O' g
    exact (OO_cancelR_conn_map O' O f g).
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
Y, X, Z: Type
f: Y -> X
g: X -> Z
H2: IsConnMap O' (g o f)
H3: IsConnMap O f
IsEquiv
  (fun x : O' Y => O_functor O' g (O_functor O' f x)) exact (isequiv_homotopic _ (O_functor_compose O' f g)).
Defined.

Definition OO_inverts_conn_map_isconnected_domain
       (O' O : ReflectiveSubuniverse) `{O << O', O <<< O', O' <= Sep O}
       {Y X : Type} (f : Y -> X)
       `{IsConnected O' Y} `{IsConnMap O _ _ f}
  : O_inverts O' f.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
Y, X: Type
f: Y -> X
H2: IsConnected O' Y
H3: IsConnMap O f
O_inverts O' f
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: O <<< O'
H1: O' <= Sep O
Y, X: Type
f: Y -> X
H2: IsConnected O' Y
H3: IsConnMap O f
O_inverts O' f
  exact (OO_inverts_conn_map_factor_conn_map O' O f (const_tt _)).
Defined.

(** Here is the converse of [ooextendable_TypeO_lex_leq]. *)
Definition O_lex_leq_extendable_TypeO
           (O' O : ReflectiveSubuniverse) `{O << O'}
           (e : forall (A:Type) (g:A->Type_ O), ExtensionAlong (to O' A) (fun _ => Type_ O) g)
  : O <<< O'.
O', O: ReflectiveSubuniverse
H: O << O'
e: forall (A : Type) (g : A -> Type_ O),
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
O <<< O'
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
e: forall (A : Type) (g : A -> Type_ O),
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
O <<< O'
  intros A; unshelve econstructor; intros P' P_inO; pose (P := fun x => (P' x ; P_inO x) : Type_ O).
O', O: ReflectiveSubuniverse
H: O << O'
e: forall (A : Type) (g : A -> Type_ O),
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
A: Type
P': A -> Type
P_inO: forall x : A, In O (P' x)
P:= fun x : A => (P' x; P_inO x) : Type_ O: A -> Type_ O
O_reflector O' A -> Type
O', O: ReflectiveSubuniverse
H: O << O'
e: forall (A : Type) (g : A -> Type_ O),
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
A: Type
P': A -> Type
P_inO: forall x : A, In O (P' x)
P:= fun x : A => (P' x; P_inO x) : Type_ O: A -> Type_ O
forall x : O_reflector O' A,
In O
  ((fun (P' : A -> Type)
      (P_inO : forall x0 : A, In O (P' x0)) =>
    let P := fun x0 : A => (P' x0; P_inO x0) : Type_ O
      in
    ?Goal) P' P_inO x)
O', O: ReflectiveSubuniverse
H: O << O'
e: forall (A : Type) (g : A -> Type_ O),
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
A: Type
P': A -> Type
P_inO: forall x : A, In O (P' x)
P:= fun x : A => (P' x; P_inO x) : Type_ O: A -> Type_ O
forall x : A,
(fun (P' : A -> Type)
   (P_inO : forall x0 : A, In O (P' x0)) =>
 let P := fun x0 : A => (P' x0; P_inO x0) : Type_ O in
 ?Goal) P' P_inO (to O' A x) <~> 
P' x
  -
O', O: ReflectiveSubuniverse
H: O << O'
e: forall (A : Type) (g : A -> Type_ O),
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
A: Type
P': A -> Type
P_inO: forall x : A, In O (P' x)
P:= fun x : A => (P' x; P_inO x) : Type_ O: A -> Type_ O
O_reflector O' A -> Type exact (fun x => ((e A P).1 x).1).
  -
O', O: ReflectiveSubuniverse
H: O << O'
e: forall (A : Type) (g : A -> Type_ O),
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
A: Type
P': A -> Type
P_inO: forall x : A, In O (P' x)
P:= fun x : A => (P' x; P_inO x) : Type_ O: A -> Type_ O
forall x : O_reflector O' A,
In O
  ((fun (P' : A -> Type)
      (P_inO : forall x0 : A, In O (P' x0)) =>
    let P := fun x0 : A => (P' x0; P_inO x0) : Type_ O
      in
    fun x0 : O_reflector O' A => ((e A P).1 x0).1) P'
     P_inO x) exact (fun x => ((e A P).1 x).2).
  -
O', O: ReflectiveSubuniverse
H: O << O'
e: forall (A : Type) (g : A -> Type_ O),
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
A: Type
P': A -> Type
P_inO: forall x : A, In O (P' x)
P:= fun x : A => (P' x; P_inO x) : Type_ O: A -> Type_ O
forall x : A,
(fun (P' : A -> Type)
   (P_inO : forall x0 : A, In O (P' x0)) =>
 let P := fun x0 : A => (P' x0; P_inO x0) : Type_ O in
 fun x0 : O_reflector O' A => ((e A P).1 x0).1) P'
  P_inO (to O' A x) <~> 
P' x intros x.
O', O: ReflectiveSubuniverse
H: O << O'
e: forall (A : Type) (g : A -> Type_ O),
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
A: Type
P': A -> Type
P_inO: forall x : A, In O (P' x)
P:= fun x : A => (P' x; P_inO x) : Type_ O: A -> Type_ O
x: A
(fun (P' : A -> Type)
   (P_inO : forall x : A, In O (P' x)) =>
 let P := fun x : A => (P' x; P_inO x) : Type_ O in
 fun x : O_reflector O' A => ((e A P).1 x).1) P' P_inO
  (to O' A x) <~> P' x
    apply equiv_path.
O', O: ReflectiveSubuniverse
H: O << O'
e: forall (A : Type) (g : A -> Type_ O),
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
A: Type
P': A -> Type
P_inO: forall x : A, In O (P' x)
P:= fun x : A => (P' x; P_inO x) : Type_ O: A -> Type_ O
x: A
(let P := fun x : A => (P' x; P_inO x) in
 fun x : O_reflector O' A => ((e A P).1 x).1)
  (to O' A x) = P' x
    exact (((e A P).2 x)..1).
Defined.

(** And a version for the accessible case. *)
Definition O_lex_leq_inO_TypeO
           (O' O : ReflectiveSubuniverse) `{O << O'}
           `{IsAccRSU O'} `{In (lift_accrsu O') (Type_ O)}
  : O <<< O'.
O', O: ReflectiveSubuniverse
H: O << O'
H0: IsAccRSU O'
H1: In (lift_accrsu O') (Type_ O)
O <<< O'
Proof.
O', O: ReflectiveSubuniverse
H: O << O'
H0: IsAccRSU O'
H1: In (lift_accrsu O') (Type_ O)
O <<< O'
  apply O_lex_leq_extendable_TypeO.
O', O: ReflectiveSubuniverse
H: O << O'
H0: IsAccRSU O'
H1: In (lift_accrsu O') (Type_ O)
forall (A : Type) (g : A -> Type_ O),
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
  intros A g.
O', O: ReflectiveSubuniverse
H: O << O'
H0: IsAccRSU O'
H1: In (lift_accrsu O') (Type_ O)
A: Type
g: A -> Type_ O
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
  assert (O_inverts (lift_accrsu O') (to O' A)).
O', O: ReflectiveSubuniverse
H: O << O'
H0: IsAccRSU O'
H1: In (lift_accrsu O') (Type_ O)
A: Type
g: A -> Type_ O
O_inverts (lift_accrsu O') (to O' A)
O', O: ReflectiveSubuniverse
H: O << O'
H0: IsAccRSU O'
H1: In (lift_accrsu O') (Type_ O)
A: Type
g: A -> Type_ O
X: O_inverts (lift_accrsu O') (to O' A)
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: IsAccRSU O'
H1: In (lift_accrsu O') (Type_ O)
A: Type
g: A -> Type_ O
O_inverts (lift_accrsu O') (to O' A) rapply (O_inverts_O_leq' (lift_accrsu O') O').
  -
O', O: ReflectiveSubuniverse
H: O << O'
H0: IsAccRSU O'
H1: In (lift_accrsu O') (Type_ O)
A: Type
g: A -> Type_ O
X: O_inverts (lift_accrsu O') (to O' A)
ExtensionAlong (to O' A)
  (fun _ : O_reflector O' A => Type_ O) g exact (fst (ooextendable_O_inverts (lift_accrsu O') (to O' A) (Type_ O) 1%nat) g).
Defined.