(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HFiber Limits.Pullback Factorization Truncations.Core.
Require Import Modality Accessible Localization Descent Separated.

Local Open Scope path_scope.
Local Open Scope subuniverse_scope.

(** * Lex modalities *)

(** A lex modality is one that preserves finite limits, or equivalently pullbacks.  Many equivalent characterizations of this can be found in Theorem 3.1 of RSS.

We choose as our definition that a lex modality to be a reflective subuniverse such that [O <<< O], which is close to (but not quite the same as) RSS Theorem 3.1 (xiii).

Note that since this includes [O << O] as a precondition, such an [O] must indeed be a modality (and since modalities coerce to reflective subuniverses, in the following notation [O] could be either an element of [ReflectiveSubuniverse] or of [Modality]). *)
Notation Lex O := (O <<< O).

(** ** Properties of lex modalities *)

(** We now show that lex modalities have all the other properties from RSS Theorem 3.1 (which are equivalent to lex-ness).  All of them are simple specializations of properties from [Descent.v] to the case [O' = O] (although in the general case they are not known to be equivalent). *)
Section LexModality.
  Context (O : Modality) `{Lex O}.

  (** RSS Theorem 3.1 (i) *)
  Definition isconnected_paths
             {A : Type} `{IsConnected O A} (x y : A)
    : IsConnected O (x = y)
    := OO_isconnected_paths O O x y.

  (** RSS Theorem 3.1 (iii) *)
  Definition conn_map_lex
             {Y X : Type} `{IsConnected O Y, IsConnected O X} (f : Y -> X)
    : IsConnMap O f
    := OO_conn_map_isconnected O O f.

  (** RSS Theorem 3.1 (iv) *)
  Definition isequiv_mapino_isconnected
         {Y X : Type} `{IsConnected O Y, IsConnected O X}
         (f : Y -> X) `{MapIn O _ _ f}
    : IsEquiv f
    := OO_isequiv_mapino_isconnected O O f.

  (** RSS Theorem 3.1 (vi) *)
  Definition 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)
    := OO_conn_map_functor_hfiber O O p b.

  (** RSS Theorem 3.1 (vii) *)
  Definition ispullback_connmap_mapino_commsq
             {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
    := OO_ispullback_connmap_mapino O O p.

  (** RSS Theorem 3.1 (viii) *)
  Global Instance conn_map_functor_hfiber_to_O
         {Y X : Type} (f : Y -> X) (x : X)
    : IsConnMap O (functor_hfiber (fun y => (to_O_natural O f y)^) x)
    := OO_conn_map_functor_hfiber_to_O O O f x.

  Global Instance isequiv_O_functor_hfiber
         {A B} (f : A -> B) (b : B)
    : IsEquiv (O_functor_hfiber O f b).
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
b: B
IsEquiv (O_functor_hfiber O f b)
  Proof.
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
b: B
IsEquiv (O_functor_hfiber O f b)
    apply (isequiv_O_rec_O_inverts O).
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
b: B
O_inverts O
  (fun X : hfiber f b =>
   (to O A X.1;
   to_O_natural O f X.1 @ ap (to O B) X.2))
    apply O_inverts_conn_map.
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
b: B
IsConnMap O
  (fun X : hfiber f b =>
   (to O A X.1;
   to_O_natural O f X.1 @ ap (to O B) X.2))
    refine (conn_map_homotopic
              O (functor_hfiber (fun x => (to_O_natural O f x)^) b)
              _ _ _).
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
b: B
functor_hfiber (fun x : A => (to_O_natural O f x)^) b ==
(fun X : hfiber f b =>
 (to O A X.1; to_O_natural O f X.1 @ ap (to O B) X.2))
    intros [a p].
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
b: B
a: A
p: f a = b
functor_hfiber (fun x : A => (to_O_natural O f x)^) b
  (a; p) =
(to O A a; to_O_natural O f a @ ap (to O B) p)
    unfold functor_hfiber, functor_sigma.
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
b: B
a: A
p: f a = b
(to O A (a; p).1;
((to_O_natural O f (a; p).1)^)^ @ ap (to O B) (a; p).2) =
(to O A a; to_O_natural O f a @ ap (to O B) p) apply ap.
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
b: B
a: A
p: f a = b
((to_O_natural O f (a; p).1)^)^ @ ap (to O B) (a; p).2 =
to_O_natural O f a @ ap (to O B) p
    apply whiskerR, inv_V.
  Defined.

  Definition equiv_O_functor_hfiber
             {A B} (f : A -> B) (b : B)
    : O (hfiber f b) <~> hfiber (O_functor O f) (to O B b)
    := Build_Equiv _ _ (O_functor_hfiber O f b) _.

  (** RSS Theorem 3.1 (ix) *)
  Global Instance isequiv_path_O
         {X : Type@{i}} (x y : X)
    : IsEquiv (path_OO O O x y)
    := isequiv_path_OO O O x y.

  Definition equiv_path_O {X : Type@{i}} (x y : X)
    : O (x = y) <~> (to O X x = to O X y)
    := equiv_path_OO O O x y.

  Definition equiv_path_O_to_O {X : Type} (x y : X)
    : (equiv_path_O x y) o (to O (x = y)) == @ap _ _ (to O X) x y.
O: Modality
Lex0: Lex O
X: Type
x, y: X
equiv_path_O x y o to O (x = y) == ap (to O X)
  Proof.
O: Modality
Lex0: Lex O
X: Type
x, y: X
equiv_path_O x y o to O (x = y) == ap (to O X)
    intros p; unfold equiv_path_O, equiv_path_OO, path_OO; cbn.
O: Modality
Lex0: Lex O
X: Type
x, y: X
p: x = y
O_rec (ap (to (modality_subuniv O) X))
  (to (modality_subuniv O) (x = y) p) =
ap (to (modality_subuniv O) X) p
    apply O_rec_beta.
  Defined.

  (** RSS Theorem 3.1 (x).  This justifies the term "left exact". *)
  Global Instance O_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))
    := OO_inverts_functor_pullback_to_O O O f g.

  Definition equiv_O_pullback {A B C : Type} (f : B -> A) (g : C -> A)
    : O (Pullback f g) <~> Pullback (O_functor O f) (O_functor O g)
    := equiv_O_rec_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)).

  Definition O_functor_pullback
             {A B C : Type} (f : B -> A) (g : C -> A)
    : IsPullback (O_functor_square O _ _ _ _ (pullback_commsq f g)).
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
IsPullback
  (O_functor_square O pullback_pr1 pullback_pr2 f g
     (pullback_commsq f g))
  Proof.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
IsPullback
  (O_functor_square O pullback_pr1 pullback_pr2 f g
     (pullback_commsq f g))
    unfold IsPullback.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
IsEquiv
  (pullback_corec
     (O_functor_square O pullback_pr1 pullback_pr2 f g
        (pullback_commsq f g)))
    nrapply (isequiv_homotopic
               (O_rec (functor_pullback _ _ _ _ _ _ _
                                        (to_O_natural O f) (to_O_natural O g)))).
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
IsEquiv
  (O_rec
     (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: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
O_rec
  (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)) ==
pullback_corec
  (O_functor_square O pullback_pr1 pullback_pr2 f g
     (pullback_commsq f g))
    1: apply isequiv_O_rec_O_inverts; exact _.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
O_rec
  (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)) ==
pullback_corec
  (O_functor_square O pullback_pr1 pullback_pr2 f g
     (pullback_commsq f g))
    apply O_indpaths.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
(fun x : Pullback f g =>
 O_rec
   (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))
   (to O (Pullback f g) x)) ==
(fun x : Pullback f g =>
 pullback_corec
   (O_functor_square O pullback_pr1 pullback_pr2 f g
      (pullback_commsq f g)) (to O (Pullback f g) x))
    etransitivity.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
(fun x : Pullback f g =>
 O_rec
   (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))
   (to O (Pullback f g) x)) == ?Goal
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
?Goal ==
(fun x : Pullback f g =>
 pullback_corec
   (O_functor_square O pullback_pr1 pullback_pr2 f g
      (pullback_commsq f g)) 
   (to O (Pullback f g) x))
    1: intro x; apply O_rec_beta.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
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) ==
(fun x : Pullback f g =>
 pullback_corec
   (O_functor_square O pullback_pr1 pullback_pr2 f g
      (pullback_commsq f g)) (to O (Pullback f g) x))
    symmetry.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
(fun x : Pullback f g =>
 pullback_corec
   (O_functor_square O pullback_pr1 pullback_pr2 f g
      (pullback_commsq f g)) (to O (Pullback f g) x)) ==
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)
    snrapply pullback_homotopic; intros [b [c e]]; cbn.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
O_functor O pullback_pr1
  (to (modality_subuniv O) (Pullback f g) (b; c; e)) =
to (modality_subuniv O) B b
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
O_functor O pullback_pr2
  (to (modality_subuniv O) (Pullback f g) (b; c; e)) =
to (modality_subuniv O) C c
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
ap (O_functor O f) ?Goal @
((to_O_natural O f b @
  ap (to (modality_subuniv O) A) e) @
 (to_O_natural O g c)^) =
O_functor_square O pullback_pr1 pullback_pr2 f g
  (pullback_commsq f g)
  (to (modality_subuniv O) (Pullback f g) (b; c; e)) @
ap (O_functor O g) ?Goal0
    all: change (to (modality_subuniv O)) with (to O).
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
O_functor O pullback_pr1
  (to O (Pullback f g) (b; c; e)) = to O B b
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
O_functor O pullback_pr2
  (to O (Pullback f g) (b; c; e)) = 
to O C c
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
ap (O_functor O f) ?Goal @
((to_O_natural O f b @ ap (to O A) e) @
 (to_O_natural O g c)^) =
O_functor_square O pullback_pr1 pullback_pr2 f g
  (pullback_commsq f g)
  (to O (Pullback f g) (b; c; e)) @
ap (O_functor O g) ?Goal0
    -
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
O_functor O pullback_pr1
  (to O (Pullback f g) (b; c; e)) = to O B b nrapply (to_O_natural O).
    -
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
O_functor O pullback_pr2
  (to O (Pullback f g) (b; c; e)) = to O C c nrapply (to_O_natural O).
    -
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
ap (O_functor O f)
  (to_O_natural O pullback_pr1 (b; c; e)) @
((to_O_natural O f b @ ap (to O A) e) @
 (to_O_natural O g c)^) =
O_functor_square O pullback_pr1 pullback_pr2 f g
  (pullback_commsq f g)
  (to O (Pullback f g) (b; c; e)) @
ap (O_functor O g)
  (to_O_natural O pullback_pr2 (b; c; e)) Open Scope long_path_scope.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
ap (O_functor O f)
  (to_O_natural O pullback_pr1 (b; c; e))
@' (to_O_natural O f b
    @' ap (to O A) e
    @' (to_O_natural O g c)^) =
O_functor_square O pullback_pr1 pullback_pr2 f g
  (pullback_commsq f g)
  (to O (Pullback f g) (b; c; e))
@' ap (O_functor O g)
     (to_O_natural O pullback_pr2 (b; c; e))
      lhs nrapply concat_p_pp.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
ap (O_functor O f)
  (to_O_natural O pullback_pr1 (b; c; e))
@' (to_O_natural O f b
    @' ap (to O A) e)
@' (to_O_natural O g c)^ =
O_functor_square O pullback_pr1 pullback_pr2 f g
  (pullback_commsq f g)
  (to O (Pullback f g) (b; c; e))
@' ap (O_functor O g)
     (to_O_natural O pullback_pr2 (b; c; e))
      lhs nrapply (concat_p_pp _ _ _ @@ 1).
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
ap (O_functor O f)
  (to_O_natural O pullback_pr1 (b; c; e))
@' to_O_natural O f b
@' ap (to O A) e
@' (to_O_natural O g c)^ =
O_functor_square O pullback_pr1 pullback_pr2 f g
  (pullback_commsq f g)
  (to O (Pullback f g) (b; c; e))
@' ap (O_functor O g)
     (to_O_natural O pullback_pr2 (b; c; e))
      rewrite to_O_natural_compose.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
(O_functor_compose O pullback_pr1 f
   (to O (Pullback f g) (b; c; e)))^
@' to_O_natural O
     (fun x : Pullback f g => f (pullback_pr1 x))
     (b; c; e)
@' ap (to O A) e
@' (to_O_natural O g c)^ =
O_functor_square O pullback_pr1 pullback_pr2 f g
  (pullback_commsq f g)
  (to O (Pullback f g) (b; c; e))
@' ap (O_functor O g)
     (to_O_natural O pullback_pr2 (b; c; e))
      unfold O_functor_square.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
(O_functor_compose O pullback_pr1 f
   (to O (Pullback f g) (b; c; e)))^
@' to_O_natural O
     (fun x : Pullback f g => f (pullback_pr1 x))
     (b; c; e)
@' ap (to O A) e
@' (to_O_natural O g c)^ =
(O_functor_compose O pullback_pr1 f
   (to O (Pullback f g) (b; c; e)))^
@' (O_functor_homotopy O
      (fun x : Pullback f g => f (pullback_pr1 x))
      (fun x : Pullback f g => g (pullback_pr2 x))
      (pullback_commsq f g)
      (to O (Pullback f g) (b; c; e))
    @' O_functor_compose O pullback_pr2 g
         (to O (Pullback f g) (b; c; e)))
@' ap (O_functor O g)
     (to_O_natural O pullback_pr2 (b; c; e))
      rewrite O_functor_homotopy_beta.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
(O_functor_compose O pullback_pr1 f
   (to O (Pullback f g) (b; c; e)))^
@' to_O_natural O
     (fun x : Pullback f g => f (pullback_pr1 x))
     (b; c; e)
@' ap (to O A) e
@' (to_O_natural O g c)^ =
(O_functor_compose O pullback_pr1 f
   (to O (Pullback f g) (b; c; e)))^
@' (to_O_natural O
      (fun x : Pullback f g => f (pullback_pr1 x))
      (b; c; e)
    @' ap (to O A) (pullback_commsq f g (b; c; e))
    @' (to_O_natural O
          (fun x : Pullback f g => g (pullback_pr2 x))
          (b; c; e))^
    @' O_functor_compose O pullback_pr2 g
         (to O (Pullback f g) (b; c; e)))
@' ap (O_functor O g)
     (to_O_natural O pullback_pr2 (b; c; e))
      rewrite 6 concat_pp_p.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
(O_functor_compose O pullback_pr1 f
   (to O (Pullback f g) (b; c; e)))^
@' (to_O_natural O
      (fun x : Pullback f g => f (pullback_pr1 x))
      (b; c; e)
    @' (ap (to O A) e
        @' (to_O_natural O g c)^)) =
(O_functor_compose O pullback_pr1 f
   (to O (Pullback f g) (b; c; e)))^
@' (to_O_natural O
      (fun x : Pullback f g => f (pullback_pr1 x))
      (b; c; e)
    @' (ap (to O A) (pullback_commsq f g (b; c; e))
        @' ((to_O_natural O
               (fun x : Pullback f g =>
                g (pullback_pr2 x)) (b; c; e))^
            @' (O_functor_compose O pullback_pr2 g
                  (to O (Pullback f g) (b; c; e))
                @' ap (O_functor O g)
                     (to_O_natural O pullback_pr2
                        (b; c; e))))))
      do 3 apply whiskerL.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
(to_O_natural O g c)^ =
(to_O_natural O
   (fun x : Pullback f g => g (pullback_pr2 x))
   (b; c; e))^
@' (O_functor_compose O pullback_pr2 g
      (to O (Pullback f g) (b; c; e))
    @' ap (O_functor O g)
         (to_O_natural O pullback_pr2 (b; c; e)))
      rhs_V nrapply concat_pp_p.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
(to_O_natural O g c)^ =
(to_O_natural O
   (fun x : Pullback f g => g (pullback_pr2 x))
   (b; c; e))^
@' O_functor_compose O pullback_pr2 g
     (to O (Pullback f g) (b; c; e))
@' ap (O_functor O g)
     (to_O_natural O pullback_pr2 (b; c; e))
      apply moveL_pM.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
(to_O_natural O g c)^
@' (ap (O_functor O g)
      (to_O_natural O pullback_pr2 (b; c; e)))^ =
(to_O_natural O
   (fun x : Pullback f g => g (pullback_pr2 x))
   (b; c; e))^
@' O_functor_compose O pullback_pr2 g
     (to O (Pullback f g) (b; c; e))
      lhs_V nrapply inv_pp.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
(ap (O_functor O g)
   (to_O_natural O pullback_pr2 (b; c; e))
 @' to_O_natural O g c)^ =
(to_O_natural O
   (fun x : Pullback f g => g (pullback_pr2 x))
   (b; c; e))^
@' O_functor_compose O pullback_pr2 g
     (to O (Pullback f g) (b; c; e))
      rhs_V nrapply inv_Vp.
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
(ap (O_functor O g)
   (to_O_natural O pullback_pr2 (b; c; e))
 @' to_O_natural O g c)^ =
((O_functor_compose O pullback_pr2 g
    (to O (Pullback f g) (b; c; e)))^
 @' to_O_natural O
      (fun x : Pullback f g => g (pullback_pr2 x))
      (b; c; e))^
      apply (ap inverse).
O: Modality
Lex0: Lex O
A, B, C: Type
f: B -> A
g: C -> A
b: B
c: C
e: f b = g c
ap (O_functor O g)
  (to_O_natural O pullback_pr2 (b; c; e))
@' to_O_natural O g c =
(O_functor_compose O pullback_pr2 g
   (to O (Pullback f g) (b; c; e)))^
@' to_O_natural O
     (fun x : Pullback f g => g (pullback_pr2 x))
     (b; c; e)
      nrapply to_O_natural_compose.
      Close Scope long_path_scope.
  Defined.

  Definition diagonal_O_functor {A B : Type} (f : A -> B)
    : diagonal (O_functor O f) == equiv_O_pullback f f o O_functor O (diagonal f).
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
diagonal (O_functor O f) ==
equiv_O_pullback f f o O_functor O (diagonal f)
  Proof.
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
diagonal (O_functor O f) ==
equiv_O_pullback f f o O_functor O (diagonal f)
    apply O_indpaths; intros x.
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
x: A
diagonal (O_functor O f) (to O A x) =
equiv_O_pullback f f
  (O_functor O (diagonal f) (to O A x))
    refine (_ @ (ap _ (to_O_natural _ _ _))^).
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
x: A
diagonal (O_functor O f) (to O A x) =
equiv_O_pullback f f
  (to O (Pullback f f) (diagonal f x))
    cbn.
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
x: A
diagonal (O_functor O f) (to (modality_subuniv O) A x) =
O_rec
  (functor_pullback f f (O_functor O f)
     (O_functor O f) (to (modality_subuniv O) B)
     (to (modality_subuniv O) A)
     (to (modality_subuniv O) A) (to_O_natural O f)
     (to_O_natural O f))
  (to (modality_subuniv O) (Pullback f f)
     (diagonal f x))
    refine (_ @ (O_rec_beta _ _)^).
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
x: A
diagonal (O_functor O f) (to (modality_subuniv O) A x) =
functor_pullback f f (O_functor O f) (O_functor O f)
  (to (modality_subuniv O) B)
  (to (modality_subuniv O) A)
  (to (modality_subuniv O) A) (to_O_natural O f)
  (to_O_natural O f) (diagonal f x)
    unfold diagonal, functor_pullback, functor_sigma; cbn.
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
x: A
(to (modality_subuniv O) A x;
to (modality_subuniv O) A x; 1) =
(to (modality_subuniv O) A x;
to (modality_subuniv O) A x;
(to_O_natural O f x @ 1) @ (to_O_natural O f x)^)
    apply ap, ap.
O: Modality
Lex0: Lex O
A, B: Type
f: A -> B
x: A
1 = (to_O_natural O f x @ 1) @ (to_O_natural O f x)^
    apply moveL_pV; exact (concat_1p_p1 _).
  Defined.

  (** RSS Theorem 3.1 (xi) *)
  Definition cancelL_conn_map
             {Y X Z : Type} (f : Y -> X) (g : X -> Z)
             `{IsConnMap O _ _ (g o f)} `{IsConnMap O _ _ g}
    : IsConnMap O f
    := OO_cancelL_conn_map O O f g.

  (** RSS Theorem 3.1 (xii) *)
  Global Instance conn_map_O_inverts
         {A B : Type} (f : A -> B) `{O_inverts O f}
    : IsConnMap O f
    := conn_map_OO_inverts O O f.

  (** RSS Theorem 3.1 (xiii) *)
  Definition modal_over_connected_isconst_lex
             (A : Type) `{IsConnected O A}
             (P : A -> Type) `{forall x, In O (P x)}
    : {Q : Type & In O Q * forall x, Q <~> P x}.
O: Modality
Lex0: Lex O
A: Type
H: IsConnected O A
P: A -> Type
H0: forall x : A, In O (P x)
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
  Proof.
O: Modality
Lex0: Lex O
A: Type
H: IsConnected O A
P: A -> Type
H0: forall x : A, In O (P x)
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
    pose proof (O_inverts_isconnected O (fun _:A => tt)).
O: Modality
Lex0: Lex O
A: Type
H: IsConnected O A
P: A -> Type
H0: forall x : A, In O (P x)
X: O_inverts O (fun _ : A => tt)
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
    exists (OO_descend_O_inverts O O (fun _:A => tt) P tt); split.
O: Modality
Lex0: Lex O
A: Type
H: IsConnected O A
P: A -> Type
H0: forall x : A, In O (P x)
X: O_inverts O (fun _ : A => tt)
In O (OO_descend_O_inverts O O (fun _ : A => tt) P tt)
O: Modality
Lex0: Lex O
A: Type
H: IsConnected O A
P: A -> Type
H0: forall x : A, In O (P x)
X: O_inverts O (fun _ : A => tt)
forall x : A,
OO_descend_O_inverts O O (fun _ : A => tt) P tt <~>
P x
    -
O: Modality
Lex0: Lex O
A: Type
H: IsConnected O A
P: A -> Type
H0: forall x : A, In O (P x)
X: O_inverts O (fun _ : A => tt)
In O (OO_descend_O_inverts O O (fun _ : A => tt) P tt) apply OO_descend_O_inverts_inO.
    -
O: Modality
Lex0: Lex O
A: Type
H: IsConnected O A
P: A -> Type
H0: forall x : A, In O (P x)
X: O_inverts O (fun _ : A => tt)
forall x : A,
OO_descend_O_inverts O O (fun _ : A => tt) P tt <~>
P x intros; nrapply OO_descend_O_inverts_beta.
  Defined.  

  (** RSS Theorem 3.11 (iii): in the accessible case, the universe is modal. *)
  Global Instance inO_typeO_lex `{Univalence} `{IsAccRSU O}
    : In (lift_accrsu O) (Type_ O)
    := _.

  (** Part of RSS Corollary 3.9: lex modalities preserve [n]-types for all [n].  This is definitely not equivalent to lex-ness, since it is true for the truncation modalities that are not lex.  But it is also not true of all modalities; e.g. the shape modality in a cohesive topos can take 0-types to [oo]-types.  With a little more work, this can probably be proven without [Funext]. *)
  Global Instance istrunc_O_lex `{Funext}
         {n : trunc_index} {A : Type} `{IsTrunc n A}
    : IsTrunc n (O A).
O: Modality
Lex0: Lex O
H: Funext
n: trunc_index
A: Type
IsTrunc0: IsTrunc n A
IsTrunc n (O A)
  Proof.
O: Modality
Lex0: Lex O
H: Funext
n: trunc_index
A: Type
IsTrunc0: IsTrunc n A
IsTrunc n (O A)
    generalize dependent A; simple_induction n n IHn; intros A ?.
O: Modality
Lex0: Lex O
H: Funext
A: Type
IsTrunc0: Contr A
Contr (O A)
O: Modality
Lex0: Lex O
H: Funext
n: trunc_index
IHn: forall A : Type, IsTrunc n A -> IsTrunc n (O A)
A: Type
IsTrunc0: IsTrunc n.+1 A
IsTrunc n.+1 (O A)
    -
O: Modality
Lex0: Lex O
H: Funext
A: Type
IsTrunc0: Contr A
Contr (O A) exact _.               (** Already proven for all modalities. *)
    -
O: Modality
Lex0: Lex O
H: Funext
n: trunc_index
IHn: forall A : Type, IsTrunc n A -> IsTrunc n (O A)
A: Type
IsTrunc0: IsTrunc n.+1 A
IsTrunc n.+1 (O A) apply istrunc_S.
O: Modality
Lex0: Lex O
H: Funext
n: trunc_index
IHn: forall A : Type, IsTrunc n A -> IsTrunc n (O A)
A: Type
IsTrunc0: IsTrunc n.+1 A
forall x y : O A, IsTrunc n (x = y)
      refine (O_ind (fun x => forall y, IsTrunc n (x = y)) _); intros x.
O: Modality
Lex0: Lex O
H: Funext
n: trunc_index
IHn: forall A : Type, IsTrunc n A -> IsTrunc n (O A)
A: Type
IsTrunc0: IsTrunc n.+1 A
x: A
forall y : O_reflector O A, IsTrunc n (to O A x = y)
      refine (O_ind (fun y => IsTrunc n (to O A x = y)) _); intros y.
O: Modality
Lex0: Lex O
H: Funext
n: trunc_index
IHn: forall A : Type, IsTrunc n A -> IsTrunc n (O A)
A: Type
IsTrunc0: IsTrunc n.+1 A
x, y: A
IsTrunc n (to O A x = to O A y)
      refine (istrunc_equiv_istrunc _ (equiv_path_O x y)).
  Defined.

End LexModality.

(** ** Equivalent characterizations of lex-ness *)

(** We will not prove that *all* of the above properties from RSS Theorem 3.1 are equivalent to lex-ness, but we will do it for some of them. *)

Section ImpliesLex.
  Context {O : Modality}.

  (** RSS 3.1 (xiii) implies lexness *)
  Definition lex_from_modal_over_connected_isconst
             (H : forall (A : Type) (A_isC : IsConnected O A)
                         (P : A -> Type) (P_inO : forall x, In O (P x)),
                 {Q : Type & In O Q * forall x, Q <~> P x})
    : Lex O.
O: Modality
H: forall A : Type,
IsConnected O A ->
forall P : A -> Type,
(forall x : A, In O (P x)) ->
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
Lex O
  Proof.
O: Modality
H: forall A : Type,
IsConnected O A ->
forall P : A -> Type,
(forall x : A, In O (P x)) ->
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
Lex O
    intros A; unshelve econstructor; intros P P_inO.
O: Modality
H: forall A : Type,
IsConnected O A ->
forall P : A -> Type,
(forall x : A, In O (P x)) ->
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
A: Type
P: A -> Type
P_inO: forall x : A, In O (P x)
O_reflector O A -> Type
O: Modality
H: forall A : Type,
IsConnected O A ->
forall P : A -> Type,
(forall x : A, In O (P x)) ->
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
A: Type
P: A -> Type
P_inO: forall x : A, In O (P x)
forall x : O_reflector O A,
In O
  ((fun (P : A -> Type)
      (P_inO : forall x0 : A, In O (P x0)) => 
    ?Goal) P P_inO x)
O: Modality
H: forall A : Type,
IsConnected O A ->
forall P : A -> Type,
(forall x : A, In O (P x)) ->
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
A: Type
P: A -> Type
P_inO: forall x : A, In O (P x)
forall x : A,
(fun (P : A -> Type)
   (P_inO : forall x0 : A, In O (P x0)) => 
 ?Goal) P P_inO (to O A x) <~> 
P x
    all:pose (Q := fun z:O A => H (hfiber (to O A) z) _ (P o pr1) _).
O: Modality
H: forall A : Type,
IsConnected O A ->
forall P : A -> Type,
(forall x : A, In O (P x)) ->
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
A: Type
P: A -> Type
P_inO: forall x : A, In O (P x)
Q:= fun z : O A =>
H (hfiber (to O A) z)
  (isconnected_hfiber_conn_map z) 
  (P o pr1)
  (fun x : hfiber (to O A) z => P_inO x.1): forall z : O A,
{Q : Type &
In O Q *
(forall x : hfiber (to O A) z, Q <~> (P o pr1) x)}
O_reflector O A -> Type
O: Modality
H: forall A : Type,
IsConnected O A ->
forall P : A -> Type,
(forall x : A, In O (P x)) ->
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
A: Type
P: A -> Type
P_inO: forall x : A, In O (P x)
Q:= fun z : O A =>
H (hfiber (to O A) z)
  (isconnected_hfiber_conn_map z) 
  (P o pr1)
  (fun x : hfiber (to O A) z => P_inO x.1): forall z : O A,
{Q : Type &
In O Q *
(forall x : hfiber (to O A) z, Q <~> (P o pr1) x)}
forall x : O_reflector O A,
In O
  ((fun (P : A -> Type)
      (P_inO : forall x0 : A, In O (P x0)) =>
    let Q :=
      fun z : O A =>
      H (hfiber (to O A) z)
        (isconnected_hfiber_conn_map z) 
        (P o pr1)
        (fun x0 : hfiber (to O A) z => P_inO x0.1) in
    ?Goal) P P_inO x)
O: Modality
H: forall A : Type,
IsConnected O A ->
forall P : A -> Type,
(forall x : A, In O (P x)) ->
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
A: Type
P: A -> Type
P_inO: forall x : A, In O (P x)
Q:= fun z : O A =>
H (hfiber (to O A) z)
  (isconnected_hfiber_conn_map z) 
  (P o pr1)
  (fun x : hfiber (to O A) z => P_inO x.1): forall z : O A,
{Q : Type &
In O Q *
(forall x : hfiber (to O A) z, Q <~> (P o pr1) x)}
forall x : A,
(fun (P : A -> Type)
   (P_inO : forall x0 : A, In O (P x0)) =>
 let Q :=
   fun z : O A =>
   H (hfiber (to O A) z)
     (isconnected_hfiber_conn_map z) 
     (P o pr1)
     (fun x0 : hfiber (to O A) z => P_inO x0.1) in
 ?Goal) P P_inO (to O A x) <~> 
P x
    -
O: Modality
H: forall A : Type,
IsConnected O A ->
forall P : A -> Type,
(forall x : A, In O (P x)) ->
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
A: Type
P: A -> Type
P_inO: forall x : A, In O (P x)
Q:= fun z : O A =>
H (hfiber (to O A) z)
  (isconnected_hfiber_conn_map z) 
  (P o pr1)
  (fun x : hfiber (to O A) z => P_inO x.1): forall z : O A,
{Q : Type &
In O Q *
(forall x : hfiber (to O A) z, Q <~> (P o pr1) x)}
O_reflector O A -> Type exact (fun z => (Q z).1).
    -
O: Modality
H: forall A : Type,
IsConnected O A ->
forall P : A -> Type,
(forall x : A, In O (P x)) ->
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
A: Type
P: A -> Type
P_inO: forall x : A, In O (P x)
Q:= fun z : O A =>
H (hfiber (to O A) z)
  (isconnected_hfiber_conn_map z) 
  (P o pr1)
  (fun x : hfiber (to O A) z => P_inO x.1): forall z : O A,
{Q : Type &
In O Q *
(forall x : hfiber (to O A) z, Q <~> (P o pr1) x)}
forall x : O_reflector O A,
In O
  ((fun (P : A -> Type)
      (P_inO : forall x0 : A, In O (P x0)) =>
    let Q :=
      fun z : O A =>
      H (hfiber (to O A) z)
        (isconnected_hfiber_conn_map z) (P o pr1)
        (fun x0 : hfiber (to O A) z => P_inO x0.1) in
    fun z : O_reflector O A => (Q z).1) P P_inO x) exact (fun z => fst (Q z).2).
    -
O: Modality
H: forall A : Type,
IsConnected O A ->
forall P : A -> Type,
(forall x : A, In O (P x)) ->
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
A: Type
P: A -> Type
P_inO: forall x : A, In O (P x)
Q:= fun z : O A =>
H (hfiber (to O A) z)
  (isconnected_hfiber_conn_map z) 
  (P o pr1)
  (fun x : hfiber (to O A) z => P_inO x.1): forall z : O A,
{Q : Type &
In O Q *
(forall x : hfiber (to O A) z, Q <~> (P o pr1) x)}
forall x : A,
(fun (P : A -> Type)
   (P_inO : forall x0 : A, In O (P x0)) =>
 let Q :=
   fun z : O A =>
   H (hfiber (to O A) z)
     (isconnected_hfiber_conn_map z) (P o pr1)
     (fun x0 : hfiber (to O A) z => P_inO x0.1) in
 fun z : O_reflector O A => (Q z).1) P P_inO
  (to O A x) <~> P x intros x; cbn.
O: Modality
H: forall A : Type,
IsConnected O A ->
forall P : A -> Type,
(forall x : A, In O (P x)) ->
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
A: Type
P: A -> Type
P_inO: forall x : A, In O (P x)
Q:= fun z : O A =>
H (hfiber (to O A) z)
  (isconnected_hfiber_conn_map z) 
  (P o pr1)
  (fun x : hfiber (to O A) z => P_inO x.1): forall z : O A,
{Q : Type &
In O Q *
(forall x : hfiber (to O A) z, Q <~> (P o pr1) x)}
x: A
(H
   (hfiber (to (modality_subuniv O) A)
      (to (modality_subuniv O) A x))
   (isconnected_hfiber_conn_map
      (to (modality_subuniv O) A x))
   (fun
      x : {x0 : A &
          to (modality_subuniv O) A x0 =
          to (modality_subuniv O) A x} => P x.1)
   (fun
      x : hfiber (to (modality_subuniv O) A)
            (to (modality_subuniv O) A x) => P_inO x.1)).1 <~>
P x
      exact (snd (Q (to O A x)).2 (x;1)).
  Defined.

  (** RSS 3.11 (iii), the universe is modal, implies lex-ness *)
  Definition lex_from_inO_typeO `{IsAccRSU O} `{In (lift_accrsu O) (Type_ O)}
    : Lex O.
O: Modality
H: IsAccRSU O
H0: In (lift_accrsu O) (Type_ O)
Lex O
  Proof.
O: Modality
H: IsAccRSU O
H0: In (lift_accrsu O) (Type_ O)
Lex O
    apply (O_lex_leq_inO_TypeO O O).
  Defined.

  (** RSS Theorem 3.1 (xi) implies lex-ness *)
  Definition lex_from_cancelL_conn_map
             (cancel : forall {Y X Z : Type} (f : Y -> X) (g : X -> Z),
                 (IsConnMap O (g o f)) -> (IsConnMap O g)
                 -> IsConnMap O f)
    : Lex O.
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
Lex O
  Proof.
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
Lex O
    apply lex_from_modal_over_connected_isconst; intros.
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
{Q : Type & In O Q * (forall x : A, Q <~> P x)}
    exists (O {x:A & P x}); split; [ exact _ | intros x; symmetry ].
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
x: A
P x <~> O {x : A & P x}
    refine (Build_Equiv _ _ (fun p => to O _ (x ; p)) _).
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
x: A
IsEquiv (fun p : P x => to O {x : A & P x} (x; p))
    nrefine (isequiv_conn_map_ino O _).
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
x: A
In O (P x)
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
x: A
In O (O_reflector O {x : A & P x})
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
x: A
IsConnMap O (fun p : P x => to O {x : A & P x} (x; p)) 1-2:exact _.
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
x: A
IsConnMap O (fun p : P x => to O {x : A & P x} (x; p))
    revert x; apply conn_map_fiber.
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
IsConnMap O
  (functor_sigma idmap
     (fun (a : A) (p : P a) =>
      to O {x : A & P x} (a; p)))
    nrefine (cancel _ _ _ _ (fun z:{x:A & O {x : A & P x}} => z.2) _ _).
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
IsConnMap O
  (fun x : {x : _ & P x} =>
   (functor_sigma idmap
      (fun (a : A) (p : P a) =>
       to O {x0 : A & P x0} (a; p)) x).2)
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
IsConnMap O (fun z : {_ : A & O {x : A & P x}} => z.2)
    1: clear cancel; exact _.
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
IsConnMap O (fun z : {_ : A & O {x : A & P x}} => z.2)
    intros z.
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
z: O {x : A & P x}
IsConnected O
  (hfiber (fun z : {_ : A & O {x : A & P x}} => z.2) z)
    refine (isconnected_equiv' O A _ _).
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
z: O {x : A & P x}
A <~>
hfiber (fun z : {_ : A & O {x : A & P x}} => z.2) z
    unfold hfiber.
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
z: O {x : A & P x}
A <~> {x : {_ : A & O {x : A & P x}} & x.2 = z}
    refine (equiv_adjointify (fun x => ((x ; z) ; 1))
                             (fun y => y.1.1) _ _).
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
z: O {x : A & P x}
(fun x : {x : {_ : A & O {x : A & P x}} & x.2 = z} =>
 (((x.1).1; z); 1)) == idmap
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
z: O {x : A & P x}
(fun x : A => (((x; z); 1).1).1) == idmap 
    -
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
z: O {x : A & P x}
(fun x : {x : {_ : A & O {x : A & P x}} & x.2 = z} =>
 (((x.1).1; z); 1)) == idmap intros [[x y] []]; reflexivity.
    -
O: Modality
cancel: forall (Y X Z : Type) (f : Y -> X)
(g : X -> Z),
IsConnMap O (g o f) ->
IsConnMap O g -> IsConnMap O f
A: Type
A_isC: IsConnected O A
P: A -> Type
P_inO: forall x : A, In O (P x)
z: O {x : A & P x}
(fun x : A => (((x; z); 1).1).1) == idmap intros x; reflexivity.
  Defined.

  (** RSS Theorem 3.1 (iii) implies lex-ness *)
  Definition lex_from_conn_map_lex
             (H : forall A B (f : A -> B),
                 (IsConnected O A) -> (IsConnected O B) ->
                 IsConnMap O f)
    : Lex O.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Lex O
  Proof.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Lex O
    apply lex_from_cancelL_conn_map.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
forall (Y X Z : Type) (f : Y -> X) (g : X -> Z),
IsConnMap O (fun x : Y => g (f x)) ->
IsConnMap O g -> IsConnMap O f
    intros Y X Z f g gfc gc x.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
IsConnected O (hfiber f x)
    pose (h := @functor_hfiber Y Z X Z (g o f) g f idmap (fun a => 1%path)).
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
h:= functor_hfiber (fun a : Y => 1): forall b : Z,
hfiber (g o f) b -> hfiber g (idmap b)
IsConnected O (hfiber f x)
    assert (cc := H _ _ (h (g x)) (gfc (g x)) (gc (g x))).
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
h:= functor_hfiber (fun a : Y => 1): forall b : Z,
hfiber (g o f) b -> hfiber g (idmap b)
cc: IsConnMap O (h (g x))
IsConnected O (hfiber f x)
    refine (isconnected_equiv' O _ _ (cc (x;1))).
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
h:= functor_hfiber (fun a : Y => 1): forall b : Z,
hfiber (g o f) b -> hfiber g (idmap b)
cc: IsConnMap O (h (g x))
hfiber (h (g x)) (x; 1) <~> hfiber f x
    unfold hfiber.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
h:= functor_hfiber (fun a : Y => 1): forall b : Z,
hfiber (g o f) b -> hfiber g (idmap b)
cc: IsConnMap O (h (g x))
{x0 : {x0 : Y & g (f x0) = g x} & h (g x) x0 = (x; 1)} <~>
{x0 : Y & f x0 = x}
    subst h; unfold functor_hfiber, functor_sigma; cbn.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g x))
{x0 : {x0 : Y & g (f x0) = g x} &
(f x0.1; 1 @ ap idmap x0.2) = (x; 1)} <~>
{x0 : Y & f x0 = x}
    refine (_ oE (equiv_sigma_assoc _ _)^-1).
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g x))
{a : Y &
{p : g (f a) = g x &
(f (a; p).1; 1 @ ap idmap (a; p).2) = (x; 1)}} <~>
{x0 : Y & f x0 = x}
    apply equiv_functor_sigma_id; intros y; cbn.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g x))
y: Y
{p : g (f y) = g x & (f y; 1 @ ap idmap p) = (x; 1)} <~>
f y = x
    refine (_ oE (equiv_functor_sigma_id _)).
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g x))
y: Y
{x : _ & ?Goal0 x} <~> f y = x
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g x))
y: Y
forall a : g (f y) = g x,
(f y; 1 @ ap idmap a) = (x; 1) <~> ?Goal0 a
    2:intros; symmetry; apply equiv_path_sigma.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g x))
y: Y
{a : g (f y) = g x &
{p : (f y; 1 @ ap idmap a).1 = (x; 1).1 &
transport (fun x0 : X => g x0 = g x) p
  (f y; 1 @ ap idmap a).2 = (x; 1).2}} <~> f y = x
    cbn.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g x))
y: Y
{a : g (f y) = g x &
{p : f y = x &
transport (fun x0 : X => g x0 = g x) p
  (1 @ ap idmap a) = 1}} <~> f y = x
    refine (_ oE equiv_sigma_symm _).
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g x))
y: Y
{b : f y = x &
{a : g (f y) = g x &
transport (fun x0 : X => g x0 = g x) b
  (1 @ ap idmap a) = 1}} <~> f y = x
    apply equiv_sigma_contr; intros p.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
x: X
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g x))
y: Y
p: f y = x
Contr
  {a : g (f y) = g x &
  transport (fun x0 : X => g x0 = g x) p
    (1 @ ap idmap a) = 1}
    destruct p; cbn.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
y: Y
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g (f y)))
Contr {a : g (f y) = g (f y) & 1 @ ap idmap a = 1}
    refine (contr_equiv' { p : g (f y) = g (f y) & p = 1%path } _).
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
y: Y
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g (f y)))
{p : g (f y) = g (f y) & p = 1} <~>
{a : g (f y) = g (f y) & 1 @ ap idmap a = 1}
    apply equiv_functor_sigma_id; intros p; cbn.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
y: Y
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g (f y)))
p: g (f y) = g (f y)
p = 1 <~> 1 @ ap idmap p = 1
    apply equiv_concat_l.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> IsConnMap O f
Y, X, Z: Type
f: Y -> X
g: X -> Z
gfc: IsConnMap O (fun x : Y => g (f x))
gc: IsConnMap O g
y: Y
cc: IsConnMap O
  (functor_hfiber (fun a : Y => 1) (g (f y)))
p: g (f y) = g (f y)
1 @ ap idmap p = p
    exact (concat_1p _ @ ap_idmap _).
  Defined.

  (** RSS Theorem 3.1 (i) implies lex-ness *)
  Definition lex_from_isconnected_paths
             (H : forall (A : Type) (Ac : IsConnected O A) (x y : A),
                 IsConnected O (x = y))
    : Lex O.
O: Modality
H: forall A : Type,
IsConnected O A ->
forall x y : A, IsConnected O (x = y)
Lex O
  Proof.
O: Modality
H: forall A : Type,
IsConnected O A ->
forall x y : A, IsConnected O (x = y)
Lex O
    apply lex_from_conn_map_lex.
O: Modality
H: forall A : Type,
IsConnected O A ->
forall x y : A, IsConnected O (x = y)
forall (A B : Type) (f : A -> B),
IsConnected O A -> IsConnected O B -> IsConnMap O f
    intros A B f Ac Bc c.
O: Modality
H: forall A : Type,
IsConnected O A ->
forall x y : A, IsConnected O (x = y)
A, B: Type
f: A -> B
Ac: IsConnected O A
Bc: IsConnected O B
c: B
IsConnected O (hfiber f c)
    rapply isconnected_sigma.
  Defined.

  (** RSS Theorem 3.1 (iv) implies lex-ness *)
  Definition lex_from_isequiv_ismodal_isconnected_types
             (H : forall A B (f : A -> B),
                 (IsConnected O A) -> (IsConnected O B) -> 
                 (MapIn O f) -> IsEquiv f)
    : Lex O.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> MapIn O f -> IsEquiv f
Lex O
  Proof.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> MapIn O f -> IsEquiv f
Lex O
    apply lex_from_conn_map_lex.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> MapIn O f -> IsEquiv f
forall (A B : Type) (f : A -> B),
IsConnected O A -> IsConnected O B -> IsConnMap O f
    intros A B f AC BC.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> MapIn O f -> IsEquiv f
A, B: Type
f: A -> B
AC: IsConnected O A
BC: IsConnected O B
IsConnMap O f
    apply (conn_map_homotopic O _ _ (fact_factors (image O f))).
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> MapIn O f -> IsEquiv f
A, B: Type
f: A -> B
AC: IsConnected O A
BC: IsConnected O B
IsConnMap O
  (fun x : A =>
   factor2 (image O f) (factor1 (image O f) x))
    apply conn_map_compose; [ exact _ | ].
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> MapIn O f -> IsEquiv f
A, B: Type
f: A -> B
AC: IsConnected O A
BC: IsConnected O B
IsConnMap O (factor2 (image O f))
    apply conn_map_isequiv.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> MapIn O f -> IsEquiv f
A, B: Type
f: A -> B
AC: IsConnected O A
BC: IsConnected O B
IsEquiv (factor2 (image O f))
    apply H; [ | exact _ | exact _ ].
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> MapIn O f -> IsEquiv f
A, B: Type
f: A -> B
AC: IsConnected O A
BC: IsConnected O B
IsConnected O (image O f)
    apply isconnected_conn_map_to_unit.
O: Modality
H: forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> MapIn O f -> IsEquiv f
A, B: Type
f: A -> B
AC: IsConnected O A
BC: IsConnected O B
IsConnMap O (const_tt (image O f))
    apply (cancelR_conn_map O (factor1 (image O f)) (const_tt _)).
  Defined.

  (** RSS Theorem 3.1 (vii) implies lex-ness *)
  Definition lex_from_ispullback_connmap_mapino_commsq
             (H : forall {A B C D}
                         (f : A -> B) (g : C -> D) (h : A -> C) (k : B -> D),
                 (IsConnMap O f) -> (IsConnMap O g) ->
                 (MapIn O h) -> (MapIn O k) ->
                 forall (p : k o f == g o h), IsPullback p)
    : Lex O.
O: Modality
H: forall (A B C D : Type) (f : A -> B) (g : C -> D)
(h : A -> C) (k : B -> D),
IsConnMap O f ->
IsConnMap O g ->
MapIn O h ->
MapIn O k ->
forall p : k o f == g o h, IsPullback p
Lex O
  Proof.
O: Modality
H: forall (A B C D : Type) (f : A -> B) (g : C -> D)
(h : A -> C) (k : B -> D),
IsConnMap O f ->
IsConnMap O g ->
MapIn O h ->
MapIn O k ->
forall p : k o f == g o h, IsPullback p
Lex O
    apply lex_from_isequiv_ismodal_isconnected_types.
O: Modality
H: forall (A B C D : Type) (f : A -> B) (g : C -> D)
(h : A -> C) (k : B -> D),
IsConnMap O f ->
IsConnMap O g ->
MapIn O h ->
MapIn O k ->
forall p : k o f == g o h, IsPullback p
forall (A B : Type) (f : A -> B),
IsConnected O A ->
IsConnected O B -> MapIn O f -> IsEquiv f
    intros A B f AC BC fM.
O: Modality
H: forall (A B C D : Type) (f : A -> B) (g : C -> D)
(h : A -> C) (k : B -> D),
IsConnMap O f ->
IsConnMap O g ->
MapIn O h ->
MapIn O k ->
forall p : k o f == g o h, IsPullback p
A, B: Type
f: A -> B
AC: IsConnected O A
BC: IsConnected O B
fM: MapIn O f
IsEquiv f
    specialize (H A Unit B Unit (const_tt _) (const_tt _) f idmap _ _ _ _
                  (fun _ => 1)).
O: Modality
A, B: Type
f: A -> B
H: IsPullback (fun x : A => 1)
AC: IsConnected O A
BC: IsConnected O B
fM: MapIn O f
IsEquiv f
    unfold IsPullback, pullback_corec in H.
O: Modality
A, B: Type
f: A -> B
H: IsEquiv (fun a : A => (const_tt A a; f a; 1))
AC: IsConnected O A
BC: IsConnected O B
fM: MapIn O f
IsEquiv f
    refine (@isequiv_compose _ _ _ H _ (fun x => x.2.1) _).
O: Modality
A, B: Type
f: A -> B
H: IsEquiv (fun a : A => (const_tt A a; f a; 1))
AC: IsConnected O A
BC: IsConnected O B
fM: MapIn O f
IsEquiv
  (fun x : Pullback idmap (const_tt B) => (x.2).1)
    unfold Pullback.
O: Modality
A, B: Type
f: A -> B
H: IsEquiv (fun a : A => (const_tt A a; f a; 1))
AC: IsConnected O A
BC: IsConnected O B
fM: MapIn O f
IsEquiv
  (fun x : {b : Unit & {c : B & b = const_tt B c}} =>
   (x.2).1)
    refine (@isequiv_compose _ {b:Unit & B}
                             (functor_sigma idmap (fun a => pr1))
                             _ _ pr2 _).
O: Modality
A, B: Type
f: A -> B
H: IsEquiv (fun a : A => (const_tt A a; f a; 1))
AC: IsConnected O A
BC: IsConnected O B
fM: MapIn O f
IsEquiv pr2
    refine (@isequiv_compose _ _ (equiv_sigma_prod0 Unit B)
                             _ _ snd _).
O: Modality
A, B: Type
f: A -> B
H: IsEquiv (fun a : A => (const_tt A a; f a; 1))
AC: IsConnected O A
BC: IsConnected O B
fM: MapIn O f
IsEquiv snd
    apply (equiv_isequiv (prod_unit_l B)).
  Defined.

End ImpliesLex.

(** ** Lex reflective subuniverses *)

(** A reflective subuniverse that preserves fibers is in fact a modality (and hence lex). *)
Definition ismodality_isequiv_O_functor_hfiber (O : ReflectiveSubuniverse)
           (H : forall {A B : Type} (f : A -> B) (b : B),
               IsEquiv (O_functor_hfiber O f b))
  : IsModality O.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
IsModality O
Proof.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
IsModality O
  intros A'; rapply reflectsD_from_inO_sigma.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
forall B : O_reflector O A' -> Type,
(forall oa : O_reflector O A', In O (B oa)) ->
In O {z : O_reflector O A' & B z}
  intros B B_inO.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
In O {z : O_reflector O A' & B z}
  pose (A := O A').
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
In O {z : O_reflector O A' & B z}
  pose (g := O_rec pr1 : O {x : A & B x} -> A).
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
In O {z : O_reflector O A' & B z}
  transparent assert (p : (forall x, g (to O _ x) = x.1)).
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) 
(b : B), IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= ?Goal: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
In O {z : O_reflector O A' & B z}
  {
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1 intros x; subst g; apply O_rec_beta. }
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
In O {z : O_reflector O A' & B z}
  apply inO_isequiv_to_O.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
IsEquiv (to O {z : O_reflector O A' & B z})
  apply isequiv_contr_map; intros x.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
Contr (hfiber (to O {z : O_reflector O A' & B z}) x)
  snrefine (contr_equiv' _ (hfiber_hfiber_compose_map _ g x)).
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
Contr
  (hfiber
     (hfiber_compose_map
        (to O {z : O_reflector O A' & B z}) g (g x))
     (x; 1))
  apply contr_map_isequiv.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
IsEquiv
  (hfiber_compose_map
     (to O {z : O_reflector O A' & B z}) g (g x))
  unfold hfiber_compose_map.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
IsEquiv
  (fun
     x0 : hfiber
            (fun x : {z : O_reflector O A' & B z} =>
             g (to O {z : O_reflector O A' & B z} x))
            (g x) =>
   (to O {z : O_reflector O A' & B z} x0.1; x0.2))
  transparent assert (h : (hfiber (@pr1 A B) (g x) <~> hfiber g (g x))).
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
hfiber pr1 (g x) <~> hfiber g (g x)
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) 
(b : B), IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
h:= ?Goal: hfiber pr1 (g x) <~> hfiber g (g x)
IsEquiv
  (fun
     x0 : hfiber
            (fun x : {z : O_reflector O A' & B z} =>
             g (to O {z : O_reflector O A' & B z} x))
            (g x) =>
   (to O {z : O_reflector O A' & B z} x0.1; x0.2))
  {
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
hfiber pr1 (g x) <~> hfiber g (g x) refine (_ oE equiv_to_O O _).
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
O (hfiber pr1 (g x)) <~> hfiber g (g x)
    refine (_ oE Build_Equiv _ _
              (O_functor_hfiber O (@pr1 A B) (g x)) _).
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
hfiber (O_functor O pr1) (to O A (g x)) <~>
hfiber g (g x)
    unfold hfiber.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
{x0 : O {x : _ & B x} &
O_functor O pr1 x0 = to O A (g x)} <~>
{x0 : O {x : A & B x} & g x0 = g x}
    apply equiv_functor_sigma_id.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
forall a : O {x : _ & B x},
O_functor O pr1 a = to O A (g x) <~> g a = g x intros y; cbn.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
y: O {x : _ & B x}
O_functor O pr1 y = to O A (g x) <~> g y = g x
    refine (_ oE (equiv_moveR_equiv_V _ _)).
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
y: O {x : _ & B x}
(to O A)^-1 (O_functor O pr1 y) = g x <~> g y = g x
    apply equiv_concat_l.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
y: O {x : _ & B x}
g y = (to O A)^-1 (O_functor O pr1 y)
    apply moveL_equiv_V.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
y: O {x : _ & B x}
to O A (g y) = O_functor O pr1 y
    unfold g, O_functor.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
y: O {x : _ & B x}
to O A (O_rec pr1 y) =
O_rec (fun x : {x : _ & B x} => to O A x.1) y
    revert y; apply O_indpaths; intros [a q]; cbn.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
q: B a
to O A (O_rec pr1 (to O {x : _ & B x} (a; q))) =
O_rec (fun x : {x : _ & B x} => to O A x.1)
  (to O {x : _ & B x} (a; q))
    refine (_ @ (O_rec_beta _ _)^).
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
q: B a
to O A (O_rec pr1 (to O {x : _ & B x} (a; q))) =
to O A a
    apply ap, O_rec_beta. }
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
h:= (equiv_functor_sigma_id
   (fun y : O {x : _ & B x} =>
    equiv_concat_l
      (moveL_equiv_V (O_functor O pr1 y) 
         (g y)
         (O_indpaths
            (fun x : O_reflector O {x : _ & B x} =>
             to O A (O_rec pr1 x))
            (O_rec
               (fun x : {x : _ & B x} => to O A x.1))
            ((fun x0 : {x : _ & B x} =>
              (fun (a : A) (q : B a) =>
               ap (to O A) (O_rec_beta pr1 ...) @
               (O_rec_beta (...) (a; q))^
               :
               to O A (O_rec pr1 ...) =
               O_rec (... => ...) (to O ... ...))
                x0.1 x0.2)
             :
             (fun x : {x : _ & B x} =>
              to O A
                (O_rec pr1 (to O {x : _ & B x} x))) ==
             (fun x : {x : _ & B x} =>
              O_rec
                (fun x0 : {x : _ & B x} =>
                 to O A x0.1)
                (to O {x : _ & B x} x))) y
          :
          to O A (g y) = O_functor O pr1 y)) 
      (g x)
    oE equiv_moveR_equiv_V 
         (O_functor O pr1 y) 
         (g x)
    :
    O_functor O pr1 y = to O A (g x) <~> g y = g x)
 :
 hfiber (O_functor O pr1) (to O A (g x)) <~>
 hfiber g (g x))
oE {|
     equiv_fun := O_functor_hfiber O pr1 (g x);
     equiv_isequiv := H {x : _ & B x} A pr1 (g x)
   |} oE equiv_to_O O (hfiber pr1 (g x)): hfiber pr1 (g x) <~> hfiber g (g x)
IsEquiv
  (fun
     x0 : hfiber
            (fun x : {z : O_reflector O A' & B z} =>
             g (to O {z : O_reflector O A' & B z} x))
            (g x) =>
   (to O {z : O_reflector O A' & B z} x0.1; x0.2))
  refine (isequiv_homotopic (h oE equiv_hfiber_homotopic _ _ p (g x)) _).
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
h:= (equiv_functor_sigma_id
   (fun y : O {x : _ & B x} =>
    equiv_concat_l
      (moveL_equiv_V (O_functor O pr1 y) 
         (g y)
         (O_indpaths
            (fun x : O_reflector O {x : _ & B x} =>
             to O A (O_rec pr1 x))
            (O_rec
               (fun x : {x : _ & B x} => to O A x.1))
            ((fun x0 : {x : _ & B x} =>
              (fun (a : A) (q : B a) =>
               ap (to O A) (O_rec_beta pr1 ...) @
               (O_rec_beta (...) (a; q))^
               :
               to O A (O_rec pr1 ...) =
               O_rec (... => ...) (to O ... ...))
                x0.1 x0.2)
             :
             (fun x : {x : _ & B x} =>
              to O A
                (O_rec pr1 (to O {x : _ & B x} x))) ==
             (fun x : {x : _ & B x} =>
              O_rec
                (fun x0 : {x : _ & B x} =>
                 to O A x0.1)
                (to O {x : _ & B x} x))) y
          :
          to O A (g y) = O_functor O pr1 y)) 
      (g x)
    oE equiv_moveR_equiv_V 
         (O_functor O pr1 y) 
         (g x)
    :
    O_functor O pr1 y = to O A (g x) <~> g y = g x)
 :
 hfiber (O_functor O pr1) (to O A (g x)) <~>
 hfiber g (g x))
oE {|
     equiv_fun := O_functor_hfiber O pr1 (g x);
     equiv_isequiv := H {x : _ & B x} A pr1 (g x)
   |} oE equiv_to_O O (hfiber pr1 (g x)): hfiber pr1 (g x) <~> hfiber g (g x)
h
oE equiv_hfiber_homotopic
     (fun x : {x : A & B x} =>
      g (to O {x0 : A & B x0} x)) pr1 p (g x) ==
(fun
   x0 : hfiber
          (fun x : {z : O_reflector O A' & B z} =>
           g (to O {z : O_reflector O A' & B z} x))
          (g x) =>
 (to O {z : O_reflector O A' & B z} x0.1; x0.2))
  intros [[a b] q]; cbn.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
h:= (equiv_functor_sigma_id
   (fun y : O {x : _ & B x} =>
    equiv_concat_l
      (moveL_equiv_V (O_functor O pr1 y) 
         (g y)
         (O_indpaths
            (fun x : O_reflector O {x : _ & B x} =>
             to O A (O_rec pr1 x))
            (O_rec
               (fun x : {x : _ & B x} => to O A x.1))
            ((fun x0 : {x : _ & B x} =>
              (fun (a : A) (q : B a) =>
               ap (to O A) (O_rec_beta pr1 ...) @
               (O_rec_beta (...) (a; q))^
               :
               to O A (O_rec pr1 ...) =
               O_rec (... => ...) (to O ... ...))
                x0.1 x0.2)
             :
             (fun x : {x : _ & B x} =>
              to O A
                (O_rec pr1 (to O {x : _ & B x} x))) ==
             (fun x : {x : _ & B x} =>
              O_rec
                (fun x0 : {x : _ & B x} =>
                 to O A x0.1)
                (to O {x : _ & B x} x))) y
          :
          to O A (g y) = O_functor O pr1 y)) 
      (g x)
    oE equiv_moveR_equiv_V 
         (O_functor O pr1 y) 
         (g x)
    :
    O_functor O pr1 y = to O A (g x) <~> g y = g x)
 :
 hfiber (O_functor O pr1) (to O A (g x)) <~>
 hfiber g (g x))
oE {|
     equiv_fun := O_functor_hfiber O pr1 (g x);
     equiv_isequiv := H {x : _ & B x} A pr1 (g x)
   |} oE equiv_to_O O (hfiber pr1 (g x)): hfiber pr1 (g x) <~> hfiber g (g x)
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
functor_sigma idmap
  (fun (a : O {x : _ & B x})
     (x0 : O_functor O pr1 a = to O A (g x)) =>
   moveL_equiv_V (O_functor O pr1 a) (g a)
     (O_indpaths
        (fun x : O_reflector O {x : _ & B x} =>
         to O A (O_rec pr1 x))
        (O_rec (fun x : {x : _ & B x} => to O A x.1))
        (fun x1 : {x : _ & B x} =>
         ap (to O A) (O_rec_beta pr1 (x1.1; x1.2)) @
         (O_rec_beta
            (fun x : {x : _ & B x} => to O A x.1)
            (x1.1; x1.2))^) a) @
   moveR_equiv_V (O_functor O pr1 a) (g x) x0)
  (O_functor_hfiber O pr1 (g x)
     (to O (hfiber pr1 (g x))
        ((a; b); (p (a; b))^ @ q))) =
(to O {z : O_reflector O A' & B z} (a; b); q) clear h.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
functor_sigma idmap
  (fun (a : O {x : _ & B x})
     (x0 : O_functor O pr1 a = to O A (g x)) =>
   moveL_equiv_V (O_functor O pr1 a) (g a)
     (O_indpaths
        (fun x : O_reflector O {x : _ & B x} =>
         to O A (O_rec pr1 x))
        (O_rec (fun x : {x : _ & B x} => to O A x.1))
        (fun x1 : {x : _ & B x} =>
         ap (to O A) (O_rec_beta pr1 (x1.1; x1.2)) @
         (O_rec_beta
            (fun x : {x : _ & B x} => to O A x.1)
            (x1.1; x1.2))^) a) @
   moveR_equiv_V (O_functor O pr1 a) (g x) x0)
  (O_functor_hfiber O pr1 (g x)
     (to O (hfiber pr1 (g x))
        ((a; b); (p (a; b))^ @ q))) =
(to O {z : O_reflector O A' & B z} (a; b); q)
  unfold O_functor_hfiber.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
functor_sigma idmap
  (fun (a : O {x : _ & B x})
     (x0 : O_functor O pr1 a = to O A (g x)) =>
   moveL_equiv_V (O_functor O pr1 a) (g a)
     (O_indpaths
        (fun x : O_reflector O {x : _ & B x} =>
         to O A (O_rec pr1 x))
        (O_rec (fun x : {x : _ & B x} => to O A x.1))
        (fun x1 : {x : _ & B x} =>
         ap (to O A) (O_rec_beta pr1 (x1.1; x1.2)) @
         (O_rec_beta
            (fun x : {x : _ & B x} => to O A x.1)
            (x1.1; x1.2))^) a) @
   moveR_equiv_V (O_functor O pr1 a) (g x) x0)
  (O_rec
     (fun X : hfiber pr1 (g x) =>
      (to O {x : _ & B x} X.1;
      to_O_natural O pr1 X.1 @ ap (to O A) X.2))
     (to O (hfiber pr1 (g x))
        ((a; b); (p (a; b))^ @ q))) =
(to O {z : O_reflector O A' & B z} (a; b); q)
  rewrite O_rec_beta.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
functor_sigma idmap
  (fun (a : O {x : _ & B x})
     (x0 : O_functor O pr1 a = to O A (g x)) =>
   moveL_equiv_V (O_functor O pr1 a) (g a)
     (O_indpaths
        (fun x : O_reflector O {x : _ & B x} =>
         to O A (O_rec pr1 x))
        (O_rec (fun x : {x : _ & B x} => to O A x.1))
        (fun x1 : {x : _ & B x} =>
         ap (to O A) (O_rec_beta pr1 (x1.1; x1.2)) @
         (O_rec_beta
            (fun x : {x : _ & B x} => to O A x.1)
            (x1.1; x1.2))^) a) @
   moveR_equiv_V (O_functor O pr1 a) (g x) x0)
  (to O {x : _ & B x} (a; b);
  to_O_natural O pr1 (a; b) @
  ap (to O A) ((p (a; b))^ @ q)) =
(to O {z : O_reflector O A' & B z} (a; b); q)
  unfold functor_sigma; cbn.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
(to O {x : _ & B x} (a; b);
moveL_equiv_V
  (O_functor O pr1 (to O {x : _ & B x} (a; b)))
  (g (to O {x : _ & B x} (a; b)))
  (O_indpaths
     (fun x : O_reflector O {x : _ & B x} =>
      to O A (O_rec pr1 x))
     (O_rec (fun x : {x : _ & B x} => to O A x.1))
     (fun x0 : {x : _ & B x} =>
      ap (to O A) (O_rec_beta pr1 (x0.1; x0.2)) @
      (O_rec_beta
         (fun x : {x : _ & B x} => to O A x.1)
         (x0.1; x0.2))^) (to O {x : _ & B x} (a; b))) @
moveR_equiv_V
  (O_functor O pr1 (to O {x : _ & B x} (a; b))) (g x)
  (to_O_natural O pr1 (a; b) @
   ap (to O A) ((p (a; b))^ @ q))) =
(to O {z : O_reflector O A' & B z} (a; b); q)
  refine (path_sigma' _ 1 _).
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
transport (fun x0 : O {x : A & B x} => g x0 = g x) 1
  (moveL_equiv_V
     (O_functor O pr1 (to O {x : _ & B x} (a; b)))
     (g (to O {x : _ & B x} (a; b)))
     (O_indpaths
        (fun x : O_reflector O {x : _ & B x} =>
         to O A (O_rec pr1 x))
        (O_rec (fun x : {x : _ & B x} => to O A x.1))
        (fun x0 : {x : _ & B x} =>
         ap (to O A) (O_rec_beta pr1 (x0.1; x0.2)) @
         (O_rec_beta
            (fun x : {x : _ & B x} => to O A x.1)
            (x0.1; x0.2))^)
        (to O {x : _ & B x} (a; b))) @
   moveR_equiv_V
     (O_functor O pr1 (to O {x : _ & B x} (a; b)))
     (g x)
     (to_O_natural O pr1 (a; b) @
      ap (to O A) ((p (a; b))^ @ q))) = q
  rewrite O_indpaths_beta; cbn.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
moveL_equiv_V
  (O_functor O pr1 (to O {x : _ & B x} (a; b)))
  (g (to O {x : _ & B x} (a; b)))
  (ap (to O A) (O_rec_beta pr1 (a; b)) @
   (O_rec_beta (fun x : {x : _ & B x} => to O A x.1)
      (a; b))^) @
moveR_equiv_V
  (O_functor O pr1 (to O {x : _ & B x} (a; b))) (g x)
  (to_O_natural O pr1 (a; b) @
   ap (to O A) ((p (a; b))^ @ q)) = q
  unfold moveL_equiv_V, moveR_equiv_V.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
((eissect (to O A) (g (to O {x : _ & B x} (a; b))))^ @
 ap (to O A)^-1
   (ap (to O A) (O_rec_beta pr1 (a; b)) @
    (O_rec_beta (fun x : {x : _ & B x} => to O A x.1)
       (a; b))^)) @
(ap (to O A)^-1
   (to_O_natural O pr1 (a; b) @
    ap (to O A) ((p (a; b))^ @ q)) @
 eissect (to O A) (g x)) = q
  Open Scope long_path_scope.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
(eissect (to O A) (g (to O {x : _ & B x} (a; b))))^
@' ap (to O A)^-1
     (ap (to O A) (O_rec_beta pr1 (a; b))
      @' (O_rec_beta
            (fun x : {x : _ & B x} => to O A x.1)
            (a; b))^)
@' (ap (to O A)^-1
      (to_O_natural O pr1 (a; b)
       @' ap (to O A) ((p (a; b))^
                       @' q))
    @' eissect (to O A) (g x)) = q
  Local Opaque eissect. (* work around bug 4533 *)
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
(eissect (to O A) (g (to O {x : _ & B x} (a; b))))^
@' ap (to O A)^-1
     (ap (to O A) (O_rec_beta pr1 (a; b))
      @' (O_rec_beta
            (fun x : {x : _ & B x} => to O A x.1)
            (a; b))^)
@' (ap (to O A)^-1
      (to_O_natural O pr1 (a; b)
       @' ap (to O A) ((p (a; b))^
                       @' q))
    @' eissect (to O A) (g x)) = q
  (* Even though https://github.com/coq/coq/issues/4533 is closed, this is still needed. *)
  rewrite !ap_pp, !concat_p_pp, !ap_V.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
(eissect (to O A) (g (to O {x : _ & B x} (a; b))))^
@' ap (to O A)^-1
     (ap (to O A) (O_rec_beta pr1 (a; b)))
@' (ap (to O A)^-1
      (O_rec_beta
         (fun x : {x : _ & B x} => to O A x.1) (a; b)))^
@' ap (to O A)^-1 (to_O_natural O pr1 (a; b))
@' (ap (to O A)^-1 (ap (to O A) (p (a; b))))^
@' ap (to O A)^-1 (ap (to O A) q)
@' eissect (to O A) (g x) = q
  unfold to_O_natural.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
(eissect (to O A) (g (to O {x : _ & B x} (a; b))))^
@' ap (to O A)^-1
     (ap (to O A) (O_rec_beta pr1 (a; b)))
@' (ap (to O A)^-1
      (O_rec_beta
         (fun x : {x : _ & B x} => to O A x.1) (a; b)))^
@' ap (to O A)^-1
     (O_rec_beta (fun x : {x : _ & B x} => to O A x.1)
        (a; b))
@' (ap (to O A)^-1 (ap (to O A) (p (a; b))))^
@' ap (to O A)^-1 (ap (to O A) q)
@' eissect (to O A) (g x) = q
  rewrite concat_pV_p.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
p:= fun x : {x : A & B x} => O_rec_beta pr1 x: forall x : {x : A & B x},
g (to O {x0 : A & B x0} x) = x.1
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
(eissect (to O A) (g (to O {x : _ & B x} (a; b))))^
@' ap (to O A)^-1
     (ap (to O A) (O_rec_beta pr1 (a; b)))
@' (ap (to O A)^-1 (ap (to O A) (p (a; b))))^
@' ap (to O A)^-1 (ap (to O A) q)
@' eissect (to O A) (g x) = q
  subst p.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
(eissect (to O A) (g (to O {x : _ & B x} (a; b))))^
@' ap (to O A)^-1
     (ap (to O A) (O_rec_beta pr1 (a; b)))
@' (ap (to O A)^-1
      (ap (to O A)
         ((fun x : {x : A & B x} => O_rec_beta pr1 x)
            (a; b))))^
@' ap (to O A)^-1 (ap (to O A) q)
@' eissect (to O A) (g x) = q
  rewrite concat_pp_V.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
(eissect (to O A) (g (to O {x : _ & B x} (a; b))))^
@' ap (to O A)^-1 (ap (to O A) q)
@' eissect (to O A) (g x) = q
  rewrite concat_pp_p; apply moveR_Vp.
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
ap (to O A)^-1 (ap (to O A) q)
@' eissect (to O A) (g x) =
eissect (to O A) (g (to O {x : _ & B x} (a; b)))
@' q
  rewrite <- !(ap_compose (to O A) (to O A)^-1).
O: ReflectiveSubuniverse
H: forall (A B : Type) (f : A -> B) (b : B),
IsEquiv (O_functor_hfiber O f b)
A': Type
B: O_reflector O A' -> Type
B_inO: forall oa : O_reflector O A', In O (B oa)
A:= O A': Type
g:= O_rec pr1 : O {x : A & B x} -> A: O {x : A & B x} -> A
x: O_reflector O {z : O_reflector O A' & B z}
a: A
b: B a
q: g (to O {x : A & B x} (a; b)) = g x
ap (fun x : A => (to O A)^-1 (to O A x)) q
@' eissect (to O A) (g x) =
eissect (to O A) (g (to O {x : _ & B x} (a; b)))
@' q
  rapply @concat_A1p.
  Local Transparent eissect. (* work around bug 4533 *)
  Close Scope long_path_scope.
Qed.

(** ** Lexness via generators *)

(** Here the characterization of when an accessible presentation yields a lex modality from Anel-Biederman-Finster-Joyal ("Higher Sheaves and Left-Exact Localizations of ∞-Topoi", arXiv:2101.02791): it's enough for path spaces of the generators to be connected. *)
Definition lex_gen `{Univalence} (O : Modality) `{IsAccModality O}
           (lexgen : forall (i : ngen_indices (acc_ngen O)) (x y : ngen_type (acc_ngen O) i),
               IsConnected O (x = y))
  : Lex O.
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
Lex O
Proof.
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
Lex O
  srapply lex_from_inO_typeO; [ exact _ | intros i ].
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
Extensions.ooExtendableAlong 
  (acc_lgen O i)
  (fun _ : lgen_codomain (acc_lgen O) i => Type_ O)
  rapply ooextendable_TypeO_from_extension; intros P; srefine (_;_).
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
forall y : lgen_codomain (acc_lgen O) i,
(fun _ : lgen_codomain (acc_lgen O) i => Type_ O) y
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
(fun
   s : forall y : lgen_codomain (acc_lgen O) i,
       (fun _ : lgen_codomain (acc_lgen O) i =>
        Type_ O) y =>
 forall x : lgen_domain (acc_lgen O) i,
 s (acc_lgen O i x) = P x) 
  ?proj1
  1:intros; exists (forall x, P x); exact _.
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
(fun
   s : forall y : lgen_codomain (acc_lgen O) i,
       (fun _ : lgen_codomain (acc_lgen O) i =>
        Type_ O) y =>
 forall x : lgen_domain (acc_lgen O) i,
 s (acc_lgen O i x) = P x)
  (fun _ : lgen_codomain (acc_lgen O) i =>
   (forall x : lgen_domain (acc_lgen O) i, P x;
   inO_forall O (lgen_domain (acc_lgen O) i)
     (fun x : lgen_domain (acc_lgen O) i => P x)
     (fun x : lgen_domain (acc_lgen O) i =>
      inO_TypeO (P x))))
  assert (wc : forall y z, P y <~> P z).
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
forall y z : lgen_domain (acc_lgen O) i, P y <~> P z
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
wc: forall y z : lgen_domain (acc_lgen O) i,
P y <~> P z
(fun
   s : forall y : lgen_codomain (acc_lgen O) i,
       (fun _ : lgen_codomain (acc_lgen O) i =>
        Type_ O) y =>
 forall x : lgen_domain (acc_lgen O) i,
 s (acc_lgen O i x) = P x)
  (fun _ : lgen_codomain (acc_lgen O) i =>
   (forall x : lgen_domain (acc_lgen O) i, P x;
   inO_forall O (lgen_domain (acc_lgen O) i)
     (fun x : lgen_domain (acc_lgen O) i => P x)
     (fun x : lgen_domain (acc_lgen O) i =>
      inO_TypeO (P x))))
  {
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
forall y z : lgen_domain (acc_lgen O) i, P y <~> P z intros y z.
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
y, z: lgen_domain (acc_lgen O) i
P y <~> P z
    (** Here we use the hypothesis [lexgen] (typeclass inference finds it automatically). *)
    refine (pr1 (isconnected_elim O _ (@equiv_transport _ P y z))). }
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
wc: forall y z : lgen_domain (acc_lgen O) i,
P y <~> P z
(fun
   s : forall y : lgen_codomain (acc_lgen O) i,
       (fun _ : lgen_codomain (acc_lgen O) i =>
        Type_ O) y =>
 forall x : lgen_domain (acc_lgen O) i,
 s (acc_lgen O i x) = P x)
  (fun _ : lgen_codomain (acc_lgen O) i =>
   (forall x : lgen_domain (acc_lgen O) i, P x;
   inO_forall O (lgen_domain (acc_lgen O) i)
     (fun x : lgen_domain (acc_lgen O) i => P x)
     (fun x : lgen_domain (acc_lgen O) i =>
      inO_TypeO (P x))))
  intros x; apply path_TypeO, path_universe_uncurried.
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
wc: forall y z : lgen_domain (acc_lgen O) i,
P y <~> P z
x: lgen_domain (acc_lgen O) i
(forall x : lgen_domain (acc_lgen O) i, P x;
inO_forall O (lgen_domain (acc_lgen O) i)
  (fun x : lgen_domain (acc_lgen O) i => P x)
  (fun x : lgen_domain (acc_lgen O) i =>
   inO_TypeO (P x))).1 <~> 
(P x).1
  refine (equiv_adjointify (fun f => f x) (fun u y => wc x y ((wc x x)^-1 u)) _ _).
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
wc: forall y z : lgen_domain (acc_lgen O) i,
P y <~> P z
x: lgen_domain (acc_lgen O) i
(fun x0 : P x => wc x x ((wc x x)^-1 x0)) == idmap
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
wc: forall y z : lgen_domain (acc_lgen O) i,
P y <~> P z
x: lgen_domain (acc_lgen O) i
(fun
   (x0 : forall x0 : lgen_domain (acc_lgen O) i, P x0)
   (y : lgen_domain (acc_lgen O) i) =>
 wc x y ((wc x x)^-1 (x0 x))) == idmap
  -
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
wc: forall y z : lgen_domain (acc_lgen O) i,
P y <~> P z
x: lgen_domain (acc_lgen O) i
(fun x0 : P x => wc x x ((wc x x)^-1 x0)) == idmap intros u; apply eisretr.
  -
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
wc: forall y z : lgen_domain (acc_lgen O) i,
P y <~> P z
x: lgen_domain (acc_lgen O) i
(fun
   (x0 : forall x0 : lgen_domain (acc_lgen O) i, P x0)
   (y : lgen_domain (acc_lgen O) i) =>
 wc x y ((wc x x)^-1 (x0 x))) == idmap intros f; apply path_forall; intros y; apply moveR_equiv_M.
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
wc: forall y z : lgen_domain (acc_lgen O) i,
P y <~> P z
x: lgen_domain (acc_lgen O) i
f: forall x0 : lgen_domain (acc_lgen O) i, P x0
y: lgen_domain (acc_lgen O) i
(wc x x)^-1 (f x) = (wc x y)^-1 (f y)
    destruct (isconnected_elim O _ (fun y => (wc x y)^-1 (f y))) as [z p].
H: Univalence
O: Modality
H0: IsAccModality O
lexgen: forall (i : ngen_indices (acc_ngen O))
(x y : acc_ngen O i), IsConnected O (x = y)
i: lgen_indices (acc_lgen O)
P: lgen_domain (acc_lgen O) i -> Type_ O
wc: forall y z : lgen_domain (acc_lgen O) i,
P y <~> P z
x: lgen_domain (acc_lgen O) i
f: forall x0 : lgen_domain (acc_lgen O) i, P x0
y: lgen_domain (acc_lgen O) i
z: P x
p: forall x0 : lgen_domain (acc_lgen O) i,
(wc x x0)^-1 (f x0) = z
(wc x x)^-1 (f x) = (wc x y)^-1 (f y)
    exact (p x @ (p y)^).
Defined.

(** ** n-fold separation *)

(** A type is [n]-[O]-separated, for n >= -2, if all its (n+2)-fold iterated identity types are [O]-modal.  Inductively, this means that it is (-2)-O-separated if it is O-modal, and (n+1)-O-separated if its identity types are n-O-separated. *)
Fixpoint nSep (n : trunc_index) (O : Subuniverse) : Subuniverse
  := match n with
     | -2 => O
     | n.+1 => Sep (nSep n O)
     end.

(** The reason for indexing this notion by a [trunc_index] rather than a [nat] is that when O is lex, a type is n-O-separated if and only if its O-unit is an n-truncated map. *)
Definition nsep_iff_trunc_to_O (n : trunc_index) (O : Modality) `{Lex O} (A : Type)
  : In (nSep n O) A <-> IsTruncMap n (to O A).
n: trunc_index
O: Modality
Lex0: Lex O
A: Type
In (nSep n O) A <-> IsTruncMap n (to O A)
Proof.
n: trunc_index
O: Modality
Lex0: Lex O
A: Type
In (nSep n O) A <-> IsTruncMap n (to O A)
  revert A; induction n as [|n IHn]; intros A; split; intros ?.
O: Modality
Lex0: Lex O
A: Type
X: In (nSep (-2) O) A
IsTruncMap (-2) (to O A)
O: Modality
Lex0: Lex O
A: Type
X: IsTruncMap (-2) (to O A)
In (nSep (-2) O) A
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: In (nSep n.+1 O) A
IsTruncMap n.+1 (to O A)
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: IsTruncMap n.+1 (to O A)
In (nSep n.+1 O) A
  -
O: Modality
Lex0: Lex O
A: Type
X: In (nSep (-2) O) A
IsTruncMap (-2) (to O A) apply contr_map_isequiv; rapply isequiv_to_O_inO.
  -
O: Modality
Lex0: Lex O
A: Type
X: IsTruncMap (-2) (to O A)
In (nSep (-2) O) A apply (inO_equiv_inO (O A) (to O A)^-1).
  -
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: In (nSep n.+1 O) A
IsTruncMap n.+1 (to O A) apply istruncmap_from_ap; intros x y.
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: In (nSep n.+1 O) A
x, y: A
IsTruncMap n (ap (to O A))
    pose (i := fst (IHn (x = y)) _).
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: In (nSep n.+1 O) A
x, y: A
i:= fst (IHn (x = y)) (inO_paths_SepO (nSep n O) x y): IsTruncMap n (to O (x = y))
IsTruncMap n (ap (to O A))
    apply istruncmap_mapinO_tr, (mapinO_homotopic _ _ (equiv_path_O_to_O O x y)).
  -
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: IsTruncMap n.+1 (to O A)
In (nSep n.+1 O) A intros x y.
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: IsTruncMap n.+1 (to O A)
x, y: A
In (nSep n O) (x = y)
    apply (snd (IHn (x = y))).
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: IsTruncMap n.+1 (to O A)
x, y: A
IsTruncMap n (to O (x = y))
    pose (i := istruncmap_ap n (to O A) x y).
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: IsTruncMap n.+1 (to O A)
x, y: A
i:= istruncmap_ap n (to O A) x y: IsTruncMap n (ap (to O A))
IsTruncMap n (to O (x = y))
    apply mapinO_tr_istruncmap in i.
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: IsTruncMap n.+1 (to O A)
x, y: A
i: MapIn (Tr n) (ap (to O A))
IsTruncMap n (to O (x = y))
    apply istruncmap_mapinO_tr, (mapinO_homotopic _ ((equiv_path_O O x y)^-1 o (@ap _ _ (to O A) x y))).
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: IsTruncMap n.+1 (to O A)
x, y: A
i: MapIn (Tr n) (ap (to O A))
(fun x0 : x = y =>
 (equiv_path_O O x y)^-1 (ap (to O A) x0)) ==
to O (x = y)
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: IsTruncMap n.+1 (to O A)
x, y: A
i: MapIn (Tr n) (ap (to O A))
MapIn (Tr n)
  (fun x0 : x = y =>
   (equiv_path_O O x y)^-1 (ap (to O A) x0))
    {
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: IsTruncMap n.+1 (to O A)
x, y: A
i: MapIn (Tr n) (ap (to O A))
(fun x0 : x = y =>
 (equiv_path_O O x y)^-1 (ap (to O A) x0)) ==
to O (x = y) intros p; apply moveR_equiv_V; symmetry; apply equiv_path_O_to_O. }
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: IsTruncMap n.+1 (to O A)
x, y: A
i: MapIn (Tr n) (ap (to O A))
MapIn (Tr n)
  (fun x0 : x = y =>
   (equiv_path_O O x y)^-1 (ap (to O A) x0))
    pose mapinO_isequiv. (* This speeds up the next line. *)
n: trunc_index
O: Modality
Lex0: Lex O
IHn: forall A : Type,
In (nSep n O) A <-> IsTruncMap n (to O A)
A: Type
X: IsTruncMap n.+1 (to O A)
x, y: A
i: MapIn (Tr n) (ap (to O A))
m:= mapinO_isequiv: forall (O : ReflectiveSubuniverse) 
(A B : Type) (f : A -> B), 
IsEquiv f -> MapIn O f
MapIn (Tr n)
  (fun x0 : x = y =>
   (equiv_path_O O x y)^-1 (ap (to O A) x0))
    rapply mapinO_compose.
Defined.