Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HFiber Extensions Factorization Limits.Pullback.
Require Export ReflectiveSubuniverse. (* [Export] because many of the lemmas and facts about reflective subuniverses are equally important for modalities. *)

Local Open Scope path_scope.

(** * Modalities *)

(** ** Dependent eliminators *)

(** A dependent version of the reflection universal property.  For later use we generalize it to refer to different subuniverses in the reflection and the elimination target. *)
Class ReflectsD@{i} (O' O : Subuniverse@{i}) (T : Type@{i})
      `{PreReflects@{i} O' T} :=
{
  extendable_to_OO :
    forall (Q : O_reflector O' T -> Type@{i}) {Q_inO : forall x, In O (Q x)},
      ooExtendableAlong (to O' T) Q
}.  

(** In particular, from this we get a dependent eliminator. *)
Definition OO_ind {O' : Subuniverse} (O : Subuniverse)
           {A : Type} `{ReflectsD O' O A}
           (B : O_reflector O' A -> Type) {B_inO : forall oa, In O (B oa)}
           (f : forall a, B (to O' A a)) (oa : O_reflector O' A)
  : B oa
  := (fst (extendable_to_OO B 1%nat) f).1 oa.

Definition OO_ind_beta {O' O : Subuniverse} {A : Type} `{ReflectsD O' O A}
           (B : O_reflector O' A -> Type) {B_inO : forall oa, In O (B oa)}
           (f : forall a, B (to O' A a)) (a : A)
  : OO_ind O B f (to O' A a) = f a
  := (fst (extendable_to_OO B 1%nat) f).2 a.

(** Conversely, if [O] is closed under path-types, a dependent eliminator suffices to prove the whole dependent universal property. *)
Definition reflectsD_from_OO_ind@{i} {O' O : Subuniverse@{i}}
           {A : Type@{i}} `{PreReflects O' A}
           (OO_ind' : forall (B : O_reflector O' A -> Type@{i})
                             (B_inO : forall oa, In O (B oa))
                             (f : forall a, B (to O' A a))
                             oa, B oa)
           (OO_ind_beta' : forall (B : O_reflector O' A -> Type@{i})
                             (B_inO : forall oa, In O (B oa))
                             (f : forall a, B (to O' A a))
                             a, OO_ind' B B_inO f (to O' A a) = f a)
           (inO_paths' : forall (B : Type@{i}) (B_inO : In O B)
                      (z z' : B), In O (z = z'))
  : ReflectsD O' O A.
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
ReflectsD O' O A
Proof.
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
ReflectsD O' O A
  constructor.
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
forall Q : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (Q x)) ->
ooExtendableAlong (to O' A) Q
  intros Q Q_inO n.
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
Q: O_reflector O' A -> Type
Q_inO: forall x : O_reflector O' A, In O (Q x)
n: nat
ExtendableAlong n (to O' A) Q
  revert Q Q_inO.
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
n: nat
forall Q : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (Q x)) ->
ExtendableAlong n (to O' A) Q simple_induction n n IHn; intros Q Q_inO.
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
Q: O_reflector O' A -> Type
Q_inO: forall x : O_reflector O' A, In O (Q x)
ExtendableAlong 0 (to O' A) Q
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
n: nat
IHn: forall Q : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (Q x)) ->
ExtendableAlong n (to O' A) Q
Q: O_reflector O' A -> Type
Q_inO: forall x : O_reflector O' A, In O (Q x)
ExtendableAlong n.+1 (to O' A) Q
  1:exact tt.
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
n: nat
IHn: forall Q : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (Q x)) ->
ExtendableAlong n (to O' A) Q
Q: O_reflector O' A -> Type
Q_inO: forall x : O_reflector O' A, In O (Q x)
ExtendableAlong n.+1 (to O' A) Q
  split.
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
n: nat
IHn: forall Q : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (Q x)) ->
ExtendableAlong n (to O' A) Q
Q: O_reflector O' A -> Type
Q_inO: forall x : O_reflector O' A, In O (Q x)
forall g : forall a : A, Q (to O' A a),
ExtensionAlong (to O' A) Q g
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
n: nat
IHn: forall Q : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (Q x)) ->
ExtendableAlong n (to O' A) Q
Q: O_reflector O' A -> Type
Q_inO: forall x : O_reflector O' A, In O (Q x)
forall h k : forall b : O_reflector O' A, Q b,
ExtendableAlong n (to O' A)
  (fun b : O_reflector O' A => h b = k b)
  -
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
n: nat
IHn: forall Q : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (Q x)) ->
ExtendableAlong n (to O' A) Q
Q: O_reflector O' A -> Type
Q_inO: forall x : O_reflector O' A, In O (Q x)
forall g : forall a : A, Q (to O' A a),
ExtensionAlong (to O' A) Q g intros g.
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
n: nat
IHn: forall Q : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (Q x)) ->
ExtendableAlong n (to O' A) Q
Q: O_reflector O' A -> Type
Q_inO: forall x : O_reflector O' A, In O (Q x)
g: forall a : A, Q (to O' A a)
ExtensionAlong (to O' A) Q g
    exists (OO_ind' Q _ g).
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
n: nat
IHn: forall Q : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (Q x)) ->
ExtendableAlong n (to O' A) Q
Q: O_reflector O' A -> Type
Q_inO: forall x : O_reflector O' A, In O (Q x)
g: forall a : A, Q (to O' A a)
forall x : A, OO_ind' Q Q_inO g (to O' A x) = g x
    rapply OO_ind_beta'.
  -
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
n: nat
IHn: forall Q : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (Q x)) ->
ExtendableAlong n (to O' A) Q
Q: O_reflector O' A -> Type
Q_inO: forall x : O_reflector O' A, In O (Q x)
forall h k : forall b : O_reflector O' A, Q b,
ExtendableAlong n (to O' A)
  (fun b : O_reflector O' A => h b = k b) intros h k.
O', O: Subuniverse
A: Type
H: PreReflects O' A
OO_ind': forall B : O_reflector O' A -> Type,
(forall oa : O_reflector O' A, In O (B oa)) ->
(forall a : A, B (to O' A a)) ->
forall oa : O_reflector O' A, B oa
OO_ind_beta': forall (B : O_reflector O' A -> Type)
(B_inO : forall oa : O_reflector O' A,
         In O (B oa))
(f : forall a : A, B (to O' A a))
(a : A),
OO_ind' B B_inO f (to O' A a) = f a
inO_paths': forall B : Type,
In O B -> forall z z' : B, In O (z = z')
n: nat
IHn: forall Q : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (Q x)) ->
ExtendableAlong n (to O' A) Q
Q: O_reflector O' A -> Type
Q_inO: forall x : O_reflector O' A, In O (Q x)
h, k: forall b : O_reflector O' A, Q b
ExtendableAlong n (to O' A)
  (fun b : O_reflector O' A => h b = k b)
    rapply IHn.
Defined.

(** In particular, this is the case if [O] is a reflective subuniverse. *)
Definition reflectsD_from_RSU {O' : Subuniverse} {O : ReflectiveSubuniverse}
           {A : Type} `{PreReflects O' A}
           (OO_ind' : forall (B : O_reflector O' A -> Type)
                             (B_inO : forall oa, In O (B oa))
                             (f : forall a, B (to O' A a))
                             oa, B oa)
           (OO_ind_beta' : forall (B : O_reflector O' A -> Type)
                             (B_inO : forall oa, In O (B oa))
                             (f : forall a, B (to O' A a))
                             a, OO_ind' B B_inO f (to O' A a) = f a)
  : ReflectsD O' O A
  := reflectsD_from_OO_ind OO_ind' OO_ind_beta' _.

(** Of course, with funext this becomes an actual equivalence. *)
Definition isequiv_oD_to_O
           {fs : Funext} (O' O : Subuniverse) {A : Type} `{ReflectsD O' O A}
           (B : O_reflector O' A -> Type) `{forall a, In O (B a)}
  : IsEquiv (fun (h : forall oa, B oa) => h oD to O' A).
fs: Funext
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: ReflectsD O' O A
B: O_reflector O' A -> Type
H1: forall a : O_reflector O' A, In O (B a)
IsEquiv
  (fun h : forall oa : O_reflector O' A, B oa =>
   h oD to O' A)
Proof.
fs: Funext
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: ReflectsD O' O A
B: O_reflector O' A -> Type
H1: forall a : O_reflector O' A, In O (B a)
IsEquiv
  (fun h : forall oa : O_reflector O' A, B oa =>
   h oD to O' A)
  apply isequiv_ooextendable, extendable_to_OO; assumption.
Defined.


(** ** The strong order *)

(** Note the reversal of the order: [O1 << O2] means that [O2] has dependent eliminators into [O1]. *)
Class O_strong_leq (O1 O2 : ReflectiveSubuniverse)
  := reflectsD_strong_leq :: forall A, ReflectsD O2 O1 A.

Infix "<<" := O_strong_leq : subuniverse_scope.
Open Scope subuniverse_scope.

(** The strong order implies the weak order. *)
Instance O_leq_strong_leq {O1 O2 : ReflectiveSubuniverse} `{O1 << O2}
  : O1 <= O2.
O1, O2: ReflectiveSubuniverse
H: O1 << O2
O1 <= O2
Proof.
O1, O2: ReflectiveSubuniverse
H: O1 << O2
O1 <= O2
  intros A A_inO1.
O1, O2: ReflectiveSubuniverse
H: O1 << O2
A: Type
A_inO1: In O1 A
In O2 A
  srapply inO_to_O_retract.
O1, O2: ReflectiveSubuniverse
H: O1 << O2
A: Type
A_inO1: In O1 A
O2 A -> A
O1, O2: ReflectiveSubuniverse
H: O1 << O2
A: Type
A_inO1: In O1 A
?mu o to O2 A == idmap
  -
O1, O2: ReflectiveSubuniverse
H: O1 << O2
A: Type
A_inO1: In O1 A
O2 A -> A exact (OO_ind O1 (fun _:O2 A => A) idmap).
  -
O1, O2: ReflectiveSubuniverse
H: O1 << O2
A: Type
A_inO1: In O1 A
OO_ind O1 (fun _ : O2 A => A) idmap o to O2 A == idmap intros a.
O1, O2: ReflectiveSubuniverse
H: O1 << O2
A: Type
A_inO1: In O1 A
a: A
OO_ind O1 (fun _ : O2 A => A) idmap (to O2 A a) = a srapply OO_ind_beta.
Defined.

(** The strong order is not obviously transitive, but it composes with the weak order on one side at least. *)
Definition O_strong_leq_trans_l (O1 O2 O3 : ReflectiveSubuniverse)
           `{O1 <= O2} `{O2 << O3}
  : O1 << O3.
O1, O2, O3: ReflectiveSubuniverse
H: O1 <= O2
H0: O2 << O3
O1 << O3
Proof.
O1, O2, O3: ReflectiveSubuniverse
H: O1 <= O2
H0: O2 << O3
O1 << O3
  intros A; constructor; intros B B_inO.
O1, O2, O3: ReflectiveSubuniverse
H: O1 <= O2
H0: O2 << O3
A: Type
B: O_reflector O3 A -> Type
B_inO: forall x : O_reflector O3 A, In O1 (B x)
ooExtendableAlong (to O3 A) B
  apply (extendable_to_OO (O := O2)).
O1, O2, O3: ReflectiveSubuniverse
H: O1 <= O2
H0: O2 << O3
A: Type
B: O_reflector O3 A -> Type
B_inO: forall x : O_reflector O3 A, In O1 (B x)
forall x : O_reflector O3 A, In O2 (B x)
  intros x.
O1, O2, O3: ReflectiveSubuniverse
H: O1 <= O2
H0: O2 << O3
A: Type
B: O_reflector O3 A -> Type
B_inO: forall x : O_reflector O3 A, In O1 (B x)
x: O_reflector O3 A
In O2 (B x)
  srapply inO_leq; exact B_inO.
Defined.


(** ** Modalities  *)

(** A modality is a reflective subuniverse with a dependent universal property with respect to itself. *)
Notation IsModality O := (O << O).

(** However, it's not clear what the best bundled definition of modality is.  The obvious one [{ O : ReflectiveSubuniverse & IsModality O}] has the advantage that bundling a reflective subuniverse into a modality and then unbundling it is definitionally the identity; but it is redundant, since the dependent universal property implies the non-dependent one, and in practice most modalities are constructed directly with a dependent eliminator.  Thus, for now at least, we take the following definition, which in RSS is called a "uniquely eliminating modality".  *)
Record Modality@{i} := Build_Modality'
{
  modality_subuniv : Subuniverse@{i} ;
  modality_prereflects : forall (T : Type@{i}),
      PreReflects modality_subuniv T ;
  modality_reflectsD :: forall (T : Type@{i}),
      ReflectsD modality_subuniv modality_subuniv T ;
}.

(** We don't declare [modality_subuniv] as a coercion or [modality_prereflects] as a global instance, because we want them only to be found by way of the following "unbundling" coercion to reflective subuniverses. *)

Definition modality_to_reflective_subuniverse (O : Modality@{i})
  : ReflectiveSubuniverse@{i}.
O: Modality
ReflectiveSubuniverse
Proof.
O: Modality
ReflectiveSubuniverse
  refine (Build_ReflectiveSubuniverse
            (modality_subuniv O) (modality_prereflects O) _).
O: Modality
forall T : Type, Reflects (modality_subuniv O) T
  intros T; constructor.
O: Modality
T: Type
forall Q : Type,
In (modality_subuniv O) Q ->
ooExtendableAlong (to (modality_subuniv O) T)
  (fun _ : O_reflector (modality_subuniv O) T => Q)
  intros Q Q_inO.
O: Modality
T, Q: Type
Q_inO: In (modality_subuniv O) Q
ooExtendableAlong (to (modality_subuniv O) T)
  (fun _ : O_reflector (modality_subuniv O) T => Q)
  srapply extendable_to_OO.
Defined.

Coercion modality_to_reflective_subuniverse : Modality >-> ReflectiveSubuniverse.

(** Unfortunately, sometimes [modality_subuniv] pops up anyway.  The following hint helps typeclass inference look through it. *)
#[export]
Hint Extern 0 (In (modality_subuniv _) _) => progress change modality_subuniv with (rsu_subuniv o modality_to_reflective_subuniverse) in * : typeclass_instances.

(** Modalities are precisely the reflective subuniverses that are [<<] themselves.  *)
Instance ismodality_modality (O : Modality) : IsModality O.
O: Modality
IsModality O
Proof.
O: Modality
IsModality O
  intros A; exact _.
Defined.

Definition modality_ismodality (O : ReflectiveSubuniverse) `{IsModality O} : Modality.
O: ReflectiveSubuniverse
IsModality0: IsModality O
Modality
Proof.
O: ReflectiveSubuniverse
IsModality0: IsModality O
Modality
  rapply Build_Modality'.
Defined.

(** When combined with [isequiv_oD_to_O], this yields Theorem 7.7.7 in the book. *)
Definition isequiv_oD_to_O_modality
           `{Funext} (O : Modality) {A : Type}
           (B : O A -> Type) `{forall a, In O (B a)}
  : IsEquiv (fun (h : forall oa, B oa) => h oD to O A).
H: Funext
O: Modality
A: Type
B: O A -> Type
H0: forall a : O A, In O (B a)
IsEquiv (fun h : forall oa : O A, B oa => h oD to O A)
Proof.
H: Funext
O: Modality
A: Type
B: O A -> Type
H0: forall a : O A, In O (B a)
IsEquiv (fun h : forall oa : O A, B oa => h oD to O A)
  srapply (isequiv_oD_to_O O O).
Defined.

(** Of course, modalities have dependent eliminators. *)
Definition O_ind {O : Subuniverse} {A : Type} `{ReflectsD O O A}
  := @OO_ind O O A _ _.
Arguments O_ind {O A _ _} B {B_inO} f oa.
Definition O_ind_beta {O : Subuniverse} {A : Type} `{ReflectsD O O A}
  := @OO_ind_beta O O A _ _.
Arguments O_ind_beta {O A _ _} B {B_inO} f a.

(** Conversely, as remarked above, we can build a modality from a dependent eliminator as long as we assume the modal types are closed under paths.  This is probably the most common way to define a modality, and one might argue that this would be a better definition of the bundled type [Modality].  For now we simply respect that by dignifying it with the unprimed constructor name [Build_Modality]. *)
Definition Build_Modality
           (In' : Type -> Type)
           (hprop_inO' : Funext -> forall T : Type, IsHProp (In' T))
           (inO_equiv_inO' : forall T U : Type,
               In' T -> forall f : T -> U, IsEquiv f -> In' U)
           (O_reflector' : Type -> Type)
           (O_inO' : forall T, In' (O_reflector' T))
           (to' : forall T, T -> O_reflector' T)
           (O_ind' : forall (A : Type) (B : O_reflector' A -> Type)
                            (B_inO : forall oa, In' (B oa))
                            (f : forall a, B (to' A a))
                            (z : O_reflector' A),
               B z)
           (O_ind_beta' : forall (A : Type) (B : O_reflector' A -> Type)
                                 (B_inO : forall oa, In' (B oa))
                                 (f : forall a, B (to' A a)) (a : A),
               O_ind' A B B_inO f (to' A a) = f a)
           (inO_paths' : forall (A : Type) (A_inO : In' A) (z z' : A),
               In' (z = z'))
  : Modality.
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
Modality
Proof.
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
Modality
  pose (O := Build_Subuniverse In' hprop_inO' inO_equiv_inO').
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
O:= {|
  In_internal := In';
  hprop_inO_internal := hprop_inO';
  inO_equiv_inO_internal := inO_equiv_inO'
|}: Subuniverse
Modality
  simple refine (Build_Modality' O _ _); intros T.
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
O:= {|
  In_internal := In';
  hprop_inO_internal := hprop_inO';
  inO_equiv_inO_internal := inO_equiv_inO'
|}: Subuniverse
T: Type
PreReflects O T
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
O:= {|
  In_internal := In';
  hprop_inO_internal := hprop_inO';
  inO_equiv_inO_internal := inO_equiv_inO'
|}: Subuniverse
T: Type
ReflectsD O O T
  -
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
O:= {|
  In_internal := In';
  hprop_inO_internal := hprop_inO';
  inO_equiv_inO_internal := inO_equiv_inO'
|}: Subuniverse
T: Type
PreReflects O T exact (Build_PreReflects O T (O_reflector' T) (O_inO' T) (to' T)).
  -
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
O:= {|
  In_internal := In';
  hprop_inO_internal := hprop_inO';
  inO_equiv_inO_internal := inO_equiv_inO'
|}: Subuniverse
T: Type
ReflectsD O O T srapply reflectsD_from_OO_ind.
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
O:= {|
  In_internal := In';
  hprop_inO_internal := hprop_inO';
  inO_equiv_inO_internal := inO_equiv_inO'
|}: Subuniverse
T: Type
forall B : O_reflector O T -> Type,
(forall oa : O_reflector O T, In O (B oa)) ->
(forall a : T, B (to O T a)) ->
forall oa : O_reflector O T, B oa
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
O:= {|
  In_internal := In';
  hprop_inO_internal := hprop_inO';
  inO_equiv_inO_internal := inO_equiv_inO'
|}: Subuniverse
T: Type
forall (B : O_reflector O T -> Type)
(B_inO : forall oa : O_reflector O T, In O (B oa))
(f : forall a : T, B (to O T a)) 
(a : T), ?OO_ind' B B_inO f (to O T a) = f a
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
O:= {|
  In_internal := In';
  hprop_inO_internal := hprop_inO';
  inO_equiv_inO_internal := inO_equiv_inO'
|}: Subuniverse
T: Type
forall B : Type,
In O B -> forall z z' : B, In O (z = z') 
    +
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
O:= {|
  In_internal := In';
  hprop_inO_internal := hprop_inO';
  inO_equiv_inO_internal := inO_equiv_inO'
|}: Subuniverse
T: Type
forall B : O_reflector O T -> Type,
(forall oa : O_reflector O T, In O (B oa)) ->
(forall a : T, B (to O T a)) ->
forall oa : O_reflector O T, B oa rapply O_ind'.
    +
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
O:= {|
  In_internal := In';
  hprop_inO_internal := hprop_inO';
  inO_equiv_inO_internal := inO_equiv_inO'
|}: Subuniverse
T: Type
forall (B : O_reflector O T -> Type)
(B_inO : forall oa : O_reflector O T, In O (B oa))
(f : forall a : T, B (to O T a)) (a : T),
O_ind' T B B_inO f (to O T a) = f a rapply O_ind_beta'.
    +
In': Type -> Type
hprop_inO': Funext ->
forall T : Type, IsHProp (In' T)
inO_equiv_inO': forall T U : Type,
In' T ->
forall f : T -> U, IsEquiv f -> In' U
O_reflector': Type -> Type
O_inO': forall T : Type, In' (O_reflector' T)
to': forall T : Type, T -> O_reflector' T
O_ind': forall (A : Type)
(B : O_reflector' A -> Type),
(forall oa : O_reflector' A, In' (B oa)) ->
(forall a : A, B (to' A a)) ->
forall z : O_reflector' A, B z
O_ind_beta': forall (A : Type)
(B : O_reflector' A -> Type)
(B_inO : forall oa : O_reflector' A,
         In' (B oa))
(f : forall a : A, B (to' A a)) 
(a : A),
O_ind' A B B_inO f (to' A a) = f a
inO_paths': forall A : Type,
In' A -> forall z z' : A, In' (z = z')
O:= {|
  In_internal := In';
  hprop_inO_internal := hprop_inO';
  inO_equiv_inO_internal := inO_equiv_inO'
|}: Subuniverse
T: Type
forall B : Type,
In O B -> forall z z' : B, In O (z = z') exact inO_paths'.
Defined.

(** A tactic that extends [strip_reflections] to modalities. It handles non-dependent elimination for reflective subuniverses and dependent elimination for modalities. [strip_truncations] does the same for truncations, but introduces fewer universe variables, so tends to work better when removing truncations. *)
Ltac strip_modalities :=
  (** Search for hypotheses of type [O X] for some [O] such that the goal is [O]-local. *)
  progress repeat
    match goal with
    | [ T : _ |- _ ]
      => revert_opaque T;
        (** Handle the non-dependent and dependent cases.  The last case requires that [O] be a modality. *)
        refine (@O_rec _ _ _ _ _ _ _) || refine (@O_indpaths _ _ _ _ _ _ _ _ _) || refine (@O_ind _ _ _ _ _ _ _);
        (** Ensure that we didn't generate more than one subgoal, i.e. that the goal was appropriately local. *)
        [];
        intro T
  end.

(** ** Dependent sums *)

(** A dependent elimination of a reflective subuniverse [O'] into [O] implies that the sum of a family of [O]-modal types over an [O']-modal type is [O']-modal.  More specifically, for a particular such sum it suffices for the [O']-reflection of that sum to dependently eliminate into [O]. *)
Instance inO_sigma_reflectsD
       {O' : ReflectiveSubuniverse} {O : Subuniverse}
       {A : Type} (B : A -> Type) `{!ReflectsD O' O (sig B)}
       `{In O' A} `{forall a, In O (B a)}
  : In O' {x:A & B x}.
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
In O' {x : A & B x}
Proof.
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
In O' {x : A & B x}
  pose (h := fun x => @O_rec O' ({x:A & B x}) A _ _ _ pr1 x).
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
In O' {x : A & B x}
  assert (p := (fun z => O_rec_beta pr1 z) : h o (to O' _) == pr1).
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: h o to O' {x : A & B x} == pr1
In O' {x : A & B x}
  pose (g := fun z => (transport B ((p z)^) z.2)).
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: h o to O' {x : A & B x} == pr1
g:= fun z : {x : A & B x} => transport B (p z)^ z.2: forall z : {x : A & B x},
B (h (to O' {x : A & B x} z))
In O' {x : A & B x}
  simpl in *.
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: (fun x : {x : A & B x} =>
 h (to O' {x0 : A & B x0} x)) == pr1
g:= fun z : {x : A & B x} => transport B (p z)^ z.2: forall z : {x : A & B x},
B (h (to O' {x : A & B x} z))
In O' {x : A & B x}
  pose (f := OO_ind O (fun x:O' (sig B) => B (h x)) g).
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: (fun x : {x : A & B x} =>
 h (to O' {x0 : A & B x0} x)) == pr1
g:= fun z : {x : A & B x} => transport B (p z)^ z.2: forall z : {x : A & B x},
B (h (to O' {x : A & B x} z))
f:= OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g: forall oa : O_reflector O' {x : _ & B x},
(fun x : O' {x : _ & B x} => B (h x)) oa
In O' {x : A & B x}
  pose (q := OO_ind_beta (fun x:O' (sig B) => B (h x)) g).
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: (fun x : {x : A & B x} =>
 h (to O' {x0 : A & B x0} x)) == pr1
g:= fun z : {x : A & B x} => transport B (p z)^ z.2: forall z : {x : A & B x},
B (h (to O' {x : A & B x} z))
f:= OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g: forall oa : O_reflector O' {x : _ & B x},
(fun x : O' {x : _ & B x} => B (h x)) oa
q:= OO_ind_beta (fun x : O' {x : _ & B x} => B (h x)) g: forall a : {x : _ & B x},
OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g
  (to O' {x : _ & B x} a) = 
g a
In O' {x : A & B x}
  apply inO_to_O_retract with (mu := fun w => (h w; f w)).
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: (fun x : {x : A & B x} =>
 h (to O' {x0 : A & B x0} x)) == pr1
g:= fun z : {x : A & B x} => transport B (p z)^ z.2: forall z : {x : A & B x},
B (h (to O' {x : A & B x} z))
f:= OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g: forall oa : O_reflector O' {x : _ & B x},
(fun x : O' {x : _ & B x} => B (h x)) oa
q:= OO_ind_beta (fun x : O' {x : _ & B x} => B (h x)) g: forall a : {x : _ & B x},
OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g
  (to O' {x : _ & B x} a) = 
g a
(fun x : {x : A & B x} =>
 (h (to O' {x0 : A & B x0} x);
 f (to O' {x0 : A & B x0} x))) == idmap
  intros [x1 x2].
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: (fun x : {x : A & B x} =>
 h (to O' {x0 : A & B x0} x)) == pr1
g:= fun z : {x : A & B x} => transport B (p z)^ z.2: forall z : {x : A & B x},
B (h (to O' {x : A & B x} z))
f:= OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g: forall oa : O_reflector O' {x : _ & B x},
(fun x : O' {x : _ & B x} => B (h x)) oa
q:= OO_ind_beta (fun x : O' {x : _ & B x} => B (h x)) g: forall a : {x : _ & B x},
OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g
  (to O' {x : _ & B x} a) = 
g a
x1: A
x2: B x1
(h (to O' {x : A & B x} (x1; x2));
f (to O' {x : A & B x} (x1; x2))) = (x1; x2)
  simple refine (path_sigma B _ _ _ _); simpl.
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: (fun x : {x : A & B x} =>
 h (to O' {x0 : A & B x0} x)) == pr1
g:= fun z : {x : A & B x} => transport B (p z)^ z.2: forall z : {x : A & B x},
B (h (to O' {x : A & B x} z))
f:= OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g: forall oa : O_reflector O' {x : _ & B x},
(fun x : O' {x : _ & B x} => B (h x)) oa
q:= OO_ind_beta (fun x : O' {x : _ & B x} => B (h x)) g: forall a : {x : _ & B x},
OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g
  (to O' {x : _ & B x} a) = 
g a
x1: A
x2: B x1
h (to O' {x : A & B x} (x1; x2)) = x1
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: (fun x : {x : A & B x} =>
 h (to O' {x0 : A & B x0} x)) == pr1
g:= fun z : {x : A & B x} => transport B (p z)^ z.2: forall z : {x : A & B x},
B (h (to O' {x : A & B x} z))
f:= OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g: forall oa : O_reflector O' {x : _ & B x},
(fun x : O' {x : _ & B x} => B (h x)) oa
q:= OO_ind_beta (fun x : O' {x : _ & B x} => B (h x)) g: forall a : {x : _ & B x},
OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g
  (to O' {x : _ & B x} a) = 
g a
x1: A
x2: B x1
transport B ?Goal (f (to O' {x : A & B x} (x1; x2))) =
x2
  -
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: (fun x : {x : A & B x} =>
 h (to O' {x0 : A & B x0} x)) == pr1
g:= fun z : {x : A & B x} => transport B (p z)^ z.2: forall z : {x : A & B x},
B (h (to O' {x : A & B x} z))
f:= OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g: forall oa : O_reflector O' {x : _ & B x},
(fun x : O' {x : _ & B x} => B (h x)) oa
q:= OO_ind_beta (fun x : O' {x : _ & B x} => B (h x)) g: forall a : {x : _ & B x},
OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g
  (to O' {x : _ & B x} a) = 
g a
x1: A
x2: B x1
h (to O' {x : A & B x} (x1; x2)) = x1 apply p.
  -
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: (fun x : {x : A & B x} =>
 h (to O' {x0 : A & B x0} x)) == pr1
g:= fun z : {x : A & B x} => transport B (p z)^ z.2: forall z : {x : A & B x},
B (h (to O' {x : A & B x} z))
f:= OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g: forall oa : O_reflector O' {x : _ & B x},
(fun x : O' {x : _ & B x} => B (h x)) oa
q:= OO_ind_beta (fun x : O' {x : _ & B x} => B (h x)) g: forall a : {x : _ & B x},
OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g
  (to O' {x : _ & B x} a) = 
g a
x1: A
x2: B x1
transport B (p (x1; x2))
  (f (to O' {x : A & B x} (x1; x2))) = x2 refine (ap _ (q (x1;x2)) @ _).
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: (fun x : {x : A & B x} =>
 h (to O' {x0 : A & B x0} x)) == pr1
g:= fun z : {x : A & B x} => transport B (p z)^ z.2: forall z : {x : A & B x},
B (h (to O' {x : A & B x} z))
f:= OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g: forall oa : O_reflector O' {x : _ & B x},
(fun x : O' {x : _ & B x} => B (h x)) oa
q:= OO_ind_beta (fun x : O' {x : _ & B x} => B (h x)) g: forall a : {x : _ & B x},
OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g
  (to O' {x : _ & B x} a) = 
g a
x1: A
x2: B x1
transport B (p (x1; x2)) (g (x1; x2)) = x2
    unfold g; simpl.
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: A -> Type
ReflectsD0: ReflectsD O' O {x : _ & B x}
H: In O' A
H0: forall a : A, In O (B a)
h:= fun x : O_reflector O' {x : A & B x} => O_rec pr1 x: O_reflector O' {x : A & B x} -> A
p: (fun x : {x : A & B x} =>
 h (to O' {x0 : A & B x0} x)) == pr1
g:= fun z : {x : A & B x} => transport B (p z)^ z.2: forall z : {x : A & B x},
B (h (to O' {x : A & B x} z))
f:= OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g: forall oa : O_reflector O' {x : _ & B x},
(fun x : O' {x : _ & B x} => B (h x)) oa
q:= OO_ind_beta (fun x : O' {x : _ & B x} => B (h x)) g: forall a : {x : _ & B x},
OO_ind O (fun x : O' {x : _ & B x} => B (h x)) g
  (to O' {x : _ & B x} a) = 
g a
x1: A
x2: B x1
transport B (p (x1; x2))
  (transport B (p (x1; x2))^ x2) = x2 exact (transport_pV B _ _).
Defined.

(** Specialized to a modality, this yields the implication (ii) => (i) from Theorem 7.7.4 of the book, and also Corollary 7.7.8, part 2. *)
Instance inO_sigma (O : Modality)
           {A:Type} (B : A -> Type) `{In O A} `{forall a, In O (B a)}
  : In O {x:A & B x}
  := _.

(** This implies that the composite of modal maps is modal. *)
Instance mapinO_compose {O : Modality} {A B C : Type} (f : A -> B) (g : B -> C)
       `{MapIn O _ _ f} `{MapIn O _ _ g}
  : MapIn O (g o f).
O: Modality
A, B, C: Type
f: A -> B
g: B -> C
H: MapIn O f
H0: MapIn O g
MapIn O (g o f)
Proof.
O: Modality
A, B, C: Type
f: A -> B
g: B -> C
H: MapIn O f
H0: MapIn O g
MapIn O (g o f)
  intros c.
O: Modality
A, B, C: Type
f: A -> B
g: B -> C
H: MapIn O f
H0: MapIn O g
c: C
In O (hfiber (fun x : A => g (f x)) c)
  exact (inO_equiv_inO' _ (hfiber_compose f g c)^-1).
Defined.

(** It also implies Corollary 7.3.10 from the book, generalized to modalities.  (Theorem 7.3.9 is true for any reflective subuniverse; we called it [equiv_O_sigma_O].) *)
Corollary equiv_sigma_inO_O {O : Modality} {A : Type} `{In O A} (P : A -> Type)
  : {x:A & O (P x)} <~> O {x:A & P x}.
O: Modality
A: Type
H: In O A
P: A -> Type
{x : A & O (P x)} <~> O {x : A & P x}
Proof.
O: Modality
A: Type
H: In O A
P: A -> Type
{x : A & O (P x)} <~> O {x : A & P x}
  transitivity (O {x:A & O (P x)}).
O: Modality
A: Type
H: In O A
P: A -> Type
{x : A & O (P x)} <~> O {x : A & O (P x)}
O: Modality
A: Type
H: In O A
P: A -> Type
O {x : A & O (P x)} <~> O {x : A & P x}
  -
O: Modality
A: Type
H: In O A
P: A -> Type
{x : A & O (P x)} <~> O {x : A & O (P x)} rapply equiv_to_O.
  -
O: Modality
A: Type
H: In O A
P: A -> Type
O {x : A & O (P x)} <~> O {x : A & P x} apply equiv_O_sigma_O.
Defined.

(** Conversely, if the sum of a particular family of [O]-modal types over an [O']-reflection is in [O'], then that family admits a dependent eliminator. *)
Definition extension_from_inO_sigma
           {O' : Subuniverse} (O : Subuniverse)
           {A:Type} `{Reflects O' A} (B: O_reflector O' A -> Type)
           {inO_sigma : In O' {z:O_reflector O' A & B z}}
           (g : forall x, B (to O' A x))
  : ExtensionAlong (to O' A) B g.
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
B: O_reflector O' A -> Type
inO_sigma: In O' {z : O_reflector O' A & B z}
g: forall x : A, B (to O' A x)
ExtensionAlong (to O' A) B g
Proof.
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
B: O_reflector O' A -> Type
inO_sigma: In O' {z : O_reflector O' A & B z}
g: forall x : A, B (to O' A x)
ExtensionAlong (to O' A) B g
  set (Z := sig B) in *.
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma: In O' Z
g: forall x : A, B (to O' A x)
ExtensionAlong (to O' A) B g
  pose (g' := (fun a:A => (to O' A a ; g a)) : A -> Z).
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma: In O' Z
g: forall x : A, B (to O' A x)
g':= (fun a : A => (to O' A a; g a)) : A -> Z: A -> Z
ExtensionAlong (to O' A) B g
  pose (f' := O_rec (O := O') g').
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma: In O' Z
g: forall x : A, B (to O' A x)
g':= (fun a : A => (to O' A a; g a)) : A -> Z: A -> Z
f':= O_rec g': O_reflector O' A -> Z
ExtensionAlong (to O' A) B g
  pose (eqf := (O_rec_beta g')  : f' o to O' A == g').
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma: In O' Z
g: forall x : A, B (to O' A x)
g':= (fun a : A => (to O' A a; g a)) : A -> Z: A -> Z
f':= O_rec g': O_reflector O' A -> Z
eqf:= O_rec_beta g' : f' o to O' A == g': f' o to O' A == g'
ExtensionAlong (to O' A) B g
  pose (eqid := O_indpaths (pr1 o f') idmap (fun x => ap@{k i} pr1 (eqf x))).
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma: In O' Z
g: forall x : A, B (to O' A x)
g':= (fun a : A => (to O' A a; g a)) : A -> Z: A -> Z
f':= O_rec g': O_reflector O' A -> Z
eqf:= O_rec_beta g' : f' o to O' A == g': f' o to O' A == g'
eqid:= O_indpaths (pr1 o f') idmap
  (fun x : A => ap pr1 (eqf x)): pr1 o f' == idmap
ExtensionAlong (to O' A) B g
  exists (fun z => transport B (eqid z) ((f' z).2)).
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma: In O' Z
g: forall x : A, B (to O' A x)
g':= (fun a : A => (to O' A a; g a)) : A -> Z: A -> Z
f':= O_rec g': O_reflector O' A -> Z
eqf:= O_rec_beta g' : f' o to O' A == g': f' o to O' A == g'
eqid:= O_indpaths (pr1 o f') idmap
  (fun x : A => ap pr1 (eqf x)): pr1 o f' == idmap
forall x : A,
transport B (eqid (to O' A x)) (f' (to O' A x)).2 =
g x
  intros a.
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma: In O' Z
g: forall x : A, B (to O' A x)
g':= (fun a : A => (to O' A a; g a)) : A -> Z: A -> Z
f':= O_rec g': O_reflector O' A -> Z
eqf:= O_rec_beta g' : f' o to O' A == g': f' o to O' A == g'
eqid:= O_indpaths (pr1 o f') idmap
  (fun x : A => ap pr1 (eqf x)): pr1 o f' == idmap
a: A
transport B (eqid (to O' A a)) (f' (to O' A a)).2 =
g a unfold eqid.
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma: In O' Z
g: forall x : A, B (to O' A x)
g':= (fun a : A => (to O' A a; g a)) : A -> Z: A -> Z
f':= O_rec g': O_reflector O' A -> Z
eqf:= O_rec_beta g' : f' o to O' A == g': f' o to O' A == g'
eqid:= O_indpaths (pr1 o f') idmap
  (fun x : A => ap pr1 (eqf x)): pr1 o f' == idmap
a: A
transport B
  (O_indpaths (fun x : O_reflector O' A => (f' x).1)
     idmap (fun x : A => ap pr1 (eqf x)) (to O' A a))
  (f' (to O' A a)).2 = g a
  refine (_ @ pr2_path (O_rec_beta g' a)).
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma: In O' Z
g: forall x : A, B (to O' A x)
g':= (fun a : A => (to O' A a; g a)) : A -> Z: A -> Z
f':= O_rec g': O_reflector O' A -> Z
eqf:= O_rec_beta g' : f' o to O' A == g': f' o to O' A == g'
eqid:= O_indpaths (pr1 o f') idmap
  (fun x : A => ap pr1 (eqf x)): pr1 o f' == idmap
a: A
transport B
  (O_indpaths (fun x : O_reflector O' A => (f' x).1)
     idmap (fun x : A => ap pr1 (eqf x)) (to O' A a))
  (f' (to O' A a)).2 =
transport B (O_rec_beta g' a) ..1
  (O_rec g' (to O' A a)).2
  refine (ap (fun p => transport B p (O_rec g' (to O' A a)).2) _).
O', O: Subuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma: In O' Z
g: forall x : A, B (to O' A x)
g':= (fun a : A => (to O' A a; g a)) : A -> Z: A -> Z
f':= O_rec g': O_reflector O' A -> Z
eqf:= O_rec_beta g' : f' o to O' A == g': f' o to O' A == g'
eqid:= O_indpaths (pr1 o f') idmap
  (fun x : A => ap pr1 (eqf x)): pr1 o f' == idmap
a: A
O_indpaths (fun x : O_reflector O' A => (f' x).1)
  idmap (fun x : A => ap pr1 (eqf x)) (to O' A a) =
(O_rec_beta g' a) ..1
  srapply O_indpaths_beta.
Defined.

(** And even a full equivalence of spaces of sections.  This is stated in CORS Proposition 2.8 (but our version avoids funext by using [ooExtendableAlong], as usual).  *)
Definition ooextendable_from_inO_sigma
           {O' : ReflectiveSubuniverse} (O : Subuniverse)
           {A : Type} (B: O_reflector O' A -> Type)
           {inO_sigma : In O' {z:O_reflector O' A & B z}}
  : ooExtendableAlong (to O' A) B.
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: O_reflector O' A -> Type
inO_sigma: In O' {z : O_reflector O' A & B z}
ooExtendableAlong (to O' A) B
Proof.
O': ReflectiveSubuniverse
O: Subuniverse
A: Type
B: O_reflector O' A -> Type
inO_sigma: In O' {z : O_reflector O' A & B z}
ooExtendableAlong (to O' A) B
  intros n; generalize dependent A.
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} ->
ExtendableAlong n (to O' A) B
  induction n as [|n IHn]; intros; [ exact tt | cbn ].
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
inO_sigma0: In O' {z : O_reflector O' A & B z}
(forall g : forall a : A, B (to O' A a),
 ExtensionAlong (to O' A) B g) *
(forall h k : forall b : O_reflector O' A, B b,
 ExtendableAlong n (to O' A)
   (fun b : O_reflector O' A => h b = k b))
  refine (extension_from_inO_sigma O B , _).
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
inO_sigma0: In O' {z : O_reflector O' A & B z}
forall h k : forall b : O_reflector O' A, B b,
ExtendableAlong n (to O' A)
  (fun b : O_reflector O' A => h b = k b)
  intros h k; napply IHn.
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
inO_sigma0: In O' {z : O_reflector O' A & B z}
h, k: forall b : O_reflector O' A, B b
In O' {z : O_reflector O' A & h z = k z}
  set (Z := sig B) in *.
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
In O' {z : O_reflector O' A & h z = k z}
  pose (W := sig (fun a => B a * B a)).
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
In O' {z : O_reflector O' A & h z = k z}
  nrefine (inO_equiv_inO' (Pullback (A := W) (fun a:O_reflector O' A => (a;(h a,k a)))
                                   (fun z:Z => (z.1;(z.2,z.2)))) _).
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
In O'
  (Pullback
     (fun a : O_reflector O' A => (a; (h a, k a)))
     (fun z : Z => (z.1; (z.2, z.2))))
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type)
(B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} ->
ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
Pullback (fun a : O_reflector O' A => (a; (h a, k a)))
  (fun z : Z => (z.1; (z.2, z.2))) <~>
{z : O_reflector O' A & h z = k z}
  {
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
In O'
  (Pullback
     (fun a : O_reflector O' A => (a; (h a, k a)))
     (fun z : Z => (z.1; (z.2, z.2)))) refine (inO_pullback O' _ _).
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
In O' W
    exact (inO_equiv_inO' _ (equiv_sigprod_pullback B B)^-1). }
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
Pullback (fun a : O_reflector O' A => (a; (h a, k a)))
  (fun z : Z => (z.1; (z.2, z.2))) <~>
{z : O_reflector O' A & h z = k z}
  unfold Pullback.
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
{b : O_reflector O' A &
{c : Z & (b; (h b, k b)) = (c.1; (c.2, c.2))}} <~>
{z : O_reflector O' A & h z = k z}
  (** The rest is just extracting paths from sigma- and product types and contracting a couple of based path spaces. *)
  apply equiv_functor_sigma_id; intros z; cbn.
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
z: O_reflector O' A
{c : Z & (z; (h z, k z)) = (c.1; (c.2, c.2))} <~>
h z = k z 
  refine (_ oE equiv_functor_sigma_id _).
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
z: O_reflector O' A
{x : _ & ?Goal0 x} <~> h z = k z
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type)
(B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} ->
ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
z: O_reflector O' A
forall a : Z,
(z; (h z, k z)) = (a.1; (a.2, a.2)) <~> ?Goal0 a
  2:intros; symmetry; apply equiv_path_sigma.
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
z: O_reflector O' A
{a : Z &
{p : (z; (h z, k z)).1 = (a.1; (a.2, a.2)).1 &
transport (fun a0 : O_reflector O' A => B a0 * B a0) p
  (z; (h z, k z)).2 = (a.1; (a.2, a.2)).2}} <~>
h z = k z
  refine (_ oE equiv_functor_sigma_id (fun z => equiv_functor_sigma_id (fun p => _))).
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
z: O_reflector O' A
{z0 : Z & {x : _ & ?Goal0@{z0:=z; z:=z0} x}} <~>
h z = k z
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type)
(B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} ->
ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
z0: O_reflector O' A
z: Z
p: (z0; (h z0, k z0)).1 = (z.1; (z.2, z.2)).1
transport (fun a : O_reflector O' A => B a * B a) p
  (z0; (h z0, k z0)).2 = 
(z.1; (z.2, z.2)).2 <~> 
?Goal0 p
  2:symmetry; apply equiv_path_prod.
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
z: O_reflector O' A
{z0 : Z &
{p : (z; (h z, k z)).1 = (z0.1; (z0.2, z0.2)).1 &
(fst
   (transport (fun a : O_reflector O' A => B a * B a)
      p (z; (h z, k z)).2) =
 fst (z0.1; (z0.2, z0.2)).2) *
(snd
   (transport (fun a : O_reflector O' A => B a * B a)
      p (z; (h z, k z)).2) =
 snd (z0.1; (z0.2, z0.2)).2)}} <~> h z = k z
  cbn.
O': ReflectiveSubuniverse
O: Subuniverse
n: nat
IHn: forall (A : Type) (B : O_reflector O' A -> Type),
In O' {z : O_reflector O' A & B z} -> ExtendableAlong n (to O' A) B
A: Type
B: O_reflector O' A -> Type
Z:= {x : _ & B x}: Type
inO_sigma0: In O' Z
h, k: forall b : O_reflector O' A, B b
W:= {a : O_reflector O' A & B a * B a}: Type
z: O_reflector O' A
{z0 : Z &
{p : z = z0.1 &
(fst
   (transport (fun a : O_reflector O' A => B a * B a)
      p (h z, k z)) = z0.2) *
(snd
   (transport (fun a : O_reflector O' A => B a * B a)
      p (h z, k z)) = z0.2)}} <~> h z = k z make_equiv_contr_basedpaths.
Defined.

(** Thus, if this holds for all sigma-types, we get the dependent universal property.  Making this an [Instance] causes typeclass search to spin.  Note the slightly different hypotheses, which mean that we can't just use the previous result: here we need only assume that the [O']-reflection of [A] exists rather than that [O'] is fully reflective, at the cost of assuming that [O] is fully reflective (although actually, closed under path-spaces would suffice). *)
Definition reflectsD_from_inO_sigma
           {O' : Subuniverse} (O : ReflectiveSubuniverse)
           {A : Type} `{Reflects O' A}
           (inO_sigma : forall (B: O_reflector O' A -> Type),
               (forall oa, In O (B oa)) -> In O' {z:O_reflector O' A & B z})
  : ReflectsD O' O A.
O': Subuniverse
O: ReflectiveSubuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
inO_sigma: 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}
ReflectsD O' O A
Proof.
O': Subuniverse
O: ReflectiveSubuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
inO_sigma: 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}
ReflectsD O' O A
  constructor; intros B B_inO.
O': Subuniverse
O: ReflectiveSubuniverse
A: Type
H: PreReflects O' A
H0: Reflects O' A
inO_sigma: 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}
B: O_reflector O' A -> Type
B_inO: forall x : O_reflector O' A, In O (B x)
ooExtendableAlong (to O' A) B
  intros n; generalize dependent A.
O': Subuniverse
O: ReflectiveSubuniverse
n: nat
forall (A : Type) (H : PreReflects O' A),
Reflects O' A ->
(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}) ->
forall B : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (B x)) ->
ExtendableAlong n (to O' A) B
  induction n as [|n IHn]; intros; [ exact tt | cbn ].
O': Subuniverse
O: ReflectiveSubuniverse
n: nat
IHn: forall (A : Type) (H : PreReflects O' A),
Reflects O' A ->
(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}) ->
forall B : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (B x)) -> ExtendableAlong n (to O' A) B
A: Type
H: PreReflects O' A
H0: Reflects O' A
inO_sigma0: 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}
B: O_reflector O' A -> Type
B_inO: forall x : O_reflector O' A, In O (B x)
(forall g : forall a : A, B (to O' A a),
 ExtensionAlong (to O' A) B g) *
(forall h k : forall b : O_reflector O' A, B b,
 ExtendableAlong n (to O' A)
   (fun b : O_reflector O' A => h b = k b))
  refine (extension_from_inO_sigma O B , _).
O': Subuniverse
O: ReflectiveSubuniverse
n: nat
IHn: forall (A : Type) (H : PreReflects O' A),
Reflects O' A ->
(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}) ->
forall B : O_reflector O' A -> Type,
(forall x : O_reflector O' A, In O (B x)) -> ExtendableAlong n (to O' A) B
A: Type
H: PreReflects O' A
H0: Reflects O' A
inO_sigma0: 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}
B: O_reflector O' A -> Type
B_inO: forall x : O_reflector O' A, In O (B x)
forall h k : forall b : O_reflector O' A, B b,
ExtendableAlong n (to O' A)
  (fun b : O_reflector O' A => h b = k b)
  intros h k; rapply IHn.
Defined.

(** In particular, we get the converse implication (i) => (ii) from Theorem 7.7.4 of the book: a reflective subuniverse closed under sigmas is a modality. *)
Definition modality_from_inO_sigma (O : ReflectiveSubuniverse)
           (H : forall (A:Type) (B:A -> Type)
                       {A_inO : In O A} `{forall a, In O (B a)},
               (In O {x:A & B x}))
  : Modality.
O: ReflectiveSubuniverse
H: forall (A : Type) (B : A -> Type),
In O A ->
(forall a : A, In O (B a)) -> In O {x : A & B x}
Modality
Proof.
O: ReflectiveSubuniverse
H: forall (A : Type) (B : A -> Type),
In O A ->
(forall a : A, In O (B a)) -> In O {x : A & B x}
Modality
  refine (Build_Modality' O _ _).
O: ReflectiveSubuniverse
H: forall (A : Type) (B : A -> Type),
In O A ->
(forall a : A, In O (B a)) -> In O {x : A & B x}
forall T : Type, ReflectsD O O T
  intros; srapply reflectsD_from_inO_sigma.
Defined.


(** ** Connectedness of the units *)

(** Dependent reflection can also be characterized by connectedness of the unit maps. *)
Instance conn_map_to_O_reflectsD {O' : Subuniverse} (O : ReflectiveSubuniverse)
       {A : Type} `{ReflectsD O' O A}
  : IsConnMap O (to O' A).
O': Subuniverse
O: ReflectiveSubuniverse
A: Type
H: PreReflects O' A
H0: ReflectsD O' O A
IsConnMap O (to O' A)
Proof.
O': Subuniverse
O: ReflectiveSubuniverse
A: Type
H: PreReflects O' A
H0: ReflectsD O' O A
IsConnMap O (to O' A)       
  apply conn_map_from_extension_elim.
O': Subuniverse
O: ReflectiveSubuniverse
A: Type
H: PreReflects O' A
H0: ReflectsD O' O A
forall P : O_reflector O' A -> Type,
(forall b : O_reflector O' A, In O (P b)) ->
forall d : forall a : A, P (to O' A a),
ExtensionAlong (to O' A) P d
  intros P P_inO f.
O': Subuniverse
O: ReflectiveSubuniverse
A: Type
H: PreReflects O' A
H0: ReflectsD O' O A
P: O_reflector O' A -> Type
P_inO: forall b : O_reflector O' A, In O (P b)
f: forall a : A, P (to O' A a)
ExtensionAlong (to O' A) P f
  exact (fst (extendable_to_OO (O := O) P 1%nat) f).
Defined.

Definition reflectsD_from_conn_map_to_O {O' : Subuniverse} (O : ReflectiveSubuniverse)
           {A : Type} `{PreReflects O' A} `{IsConnMap O _ _ (to O' A)}
  : ReflectsD O' O A.
O': Subuniverse
O: ReflectiveSubuniverse
A: Type
H: PreReflects O' A
H0: IsConnMap O (to O' A)
ReflectsD O' O A
Proof.
O': Subuniverse
O: ReflectiveSubuniverse
A: Type
H: PreReflects O' A
H0: IsConnMap O (to O' A)
ReflectsD O' O A
  constructor; rapply ooextendable_conn_map_inO.
Defined.

(** In particular, if [O1 << O2] then every [O2]-unit is [O1]-connected. *)
Instance conn_map_to_O_strong_leq
       {O1 O2 : ReflectiveSubuniverse} `{O1 << O2} (A : Type)
  : IsConnMap O1 (to O2 A)
  := _.

(** Thus, if [O] is a modality, then every [O]-unit is [O]-connected.  This is Corollary 7.5.8 in the book. *)
Instance conn_map_to_O {O : Modality} (A : Type)
  : IsConnMap O (to O A)
  := _.

(** When [O1 << O2], [O_functor O2] preserves [O1]-connected maps. *)
Proposition conn_map_O_functor_strong_leq {O1 O2 : ReflectiveSubuniverse} (leq : O1 << O2)
  {X Y : Type} (f : X -> Y) `{IsConnMap O1 _ _ f}
  : IsConnMap O1 (O_functor O2 f).
O1, O2: ReflectiveSubuniverse
leq: O1 << O2
X, Y: Type
f: X -> Y
H: IsConnMap O1 f
IsConnMap O1 (O_functor O2 f)
Proof.
O1, O2: ReflectiveSubuniverse
leq: O1 << O2
X, Y: Type
f: X -> Y
H: IsConnMap O1 f
IsConnMap O1 (O_functor O2 f)
  rapply (cancelR_conn_map _ (to O2 _)).
O1, O2: ReflectiveSubuniverse
leq: O1 << O2
X, Y: Type
f: X -> Y
H: IsConnMap O1 f
IsConnMap O1 (fun x : X => O_functor O2 f (to O2 X x))
  napply conn_map_homotopic.
O1, O2: ReflectiveSubuniverse
leq: O1 << O2
X, Y: Type
f: X -> Y
H: IsConnMap O1 f
?Goal == (fun x : X => O_functor O2 f (to O2 X x))
O1, O2: ReflectiveSubuniverse
leq: O1 << O2
X, Y: Type
f: X -> Y
H: IsConnMap O1 f
IsConnMap O1 ?Goal
  1: symmetry; apply to_O_natural.
O1, O2: ReflectiveSubuniverse
leq: O1 << O2
X, Y: Type
f: X -> Y
H: IsConnMap O1 f
IsConnMap O1 (fun x : X => to O2 Y (f x))
  rapply conn_map_compose.
Defined.


(** ** Easy modalities *)

(** The book uses yet a different definition of modality, which requires an induction principle only into families of the form [fun oa => O (B oa)], and similarly only that path-spaces of types [O A] are "modal" in the sense that the unit is an equivalence.  As shown in section 1 of RSS, this is equivalent, roughly since every modal type [A] (in this sense) is equivalent to [O A].

Our definitions are more convenient in formalized applications because in some examples (such as [Trunc] and closed modalities), there is a naturally occurring [O_ind] into all modal types that is not judgmentally equal to the one that can be constructed by passing through [O] and back again.  Thus, when we apply general theorems about modalities to a particular modality such as [Trunc], the proofs will reduce definitionally to "the way we would have proved them directly" if we didn't know about general modalities.

On the other hand, in other examples (such as [~~] and open modalities) it is easier to construct the latter weaker induction principle.  Thus, we now show how to get from that to our definition of modality. *)

Section EasyModalities.

  Universe i.
  Context (O_reflector : Type@{i} -> Type@{i})
          (to : forall (T : Type@{i}), T -> O_reflector T)
          (O_indO
           : forall (A : Type@{i})
                    (B : O_reflector A -> Type@{i})
                    (f : forall a, O_reflector (B (to A a)))
                    (z : O_reflector A),
              O_reflector (B z))
          (O_indO_beta
           : forall (A : Type@{i})
                    (B : O_reflector A -> Type@{i})
                    (f : forall a, O_reflector (B (to A a))) (a : A),
              O_indO A B f (to A a) = f a)
          (inO_pathsO
           : forall (A : Type@{i}) (z z' : O_reflector A),
              IsEquiv (to (z = z'))).

  Local Definition In_easy : Type@{i} -> Type@{i}
    := fun A => IsEquiv (to A).

  Local Definition O_ind_easy
             (A : Type) (B : O_reflector A -> Type)
             (B_inO : forall oa, In_easy (B oa))
    : (forall a, B (to A a)) -> forall oa, B oa.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
B: O_reflector A -> Type
B_inO: forall oa : O_reflector A, In_easy (B oa)
(forall a : A, B (to A a)) ->
forall oa : O_reflector A, B oa
  Proof.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
B: O_reflector A -> Type
B_inO: forall oa : O_reflector A, In_easy (B oa)
(forall a : A, B (to A a)) ->
forall oa : O_reflector A, B oa
    simpl; intros f oa.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
B: O_reflector A -> Type
B_inO: forall oa : O_reflector A, In_easy (B oa)
f: forall a : A, B (to A a)
oa: O_reflector A
B oa
    pose (H := B_inO oa); unfold In_easy in H.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
B: O_reflector A -> Type
B_inO: forall oa : O_reflector A, In_easy (B oa)
f: forall a : A, B (to A a)
oa: O_reflector A
H:= B_inO oa: IsEquiv (to (B oa))
B oa
    apply ((to (B oa))^-1).
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
B: O_reflector A -> Type
B_inO: forall oa : O_reflector A, In_easy (B oa)
f: forall a : A, B (to A a)
oa: O_reflector A
H:= B_inO oa: IsEquiv (to (B oa))
O_reflector (B oa)
    apply O_indO.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
B: O_reflector A -> Type
B_inO: forall oa : O_reflector A, In_easy (B oa)
f: forall a : A, B (to A a)
oa: O_reflector A
H:= B_inO oa: IsEquiv (to (B oa))
forall a : A, O_reflector (B (to A a))
    intros a; apply to, f.
  Defined.

  Local Definition O_ind_easy_beta
             (A : Type) (B : O_reflector A -> Type)
             (B_inO : forall oa, In_easy (B oa))
             (f : forall a : A, B (to A a)) (a:A)
  : O_ind_easy A B B_inO f (to A a) = f a.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
B: O_reflector A -> Type
B_inO: forall oa : O_reflector A, In_easy (B oa)
f: forall a : A, B (to A a)
a: A
O_ind_easy A B B_inO f (to A a) = f a
  Proof.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
B: O_reflector A -> Type
B_inO: forall oa : O_reflector A, In_easy (B oa)
f: forall a : A, B (to A a)
a: A
O_ind_easy A B B_inO f (to A a) = f a
    unfold O_ind_easy.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
B: O_reflector A -> Type
B_inO: forall oa : O_reflector A, In_easy (B oa)
f: forall a : A, B (to A a)
a: A
(to (B (to A a)))^-1
  (O_indO A B (fun a : A => to (B (to A a)) (f a))
     (to A a)) = f a
    apply moveR_equiv_V.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
B: O_reflector A -> Type
B_inO: forall oa : O_reflector A, In_easy (B oa)
f: forall a : A, B (to A a)
a: A
O_indO A B (fun a : A => to (B (to A a)) (f a))
  (to A a) = to (B (to A a)) (f a)
    apply @O_indO_beta with (f := fun x => to _ (f x)).
  Qed.

  Local Definition O_inO_easy (A : Type) : In_easy (O_reflector A).
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
In_easy (O_reflector A)
  Proof.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
In_easy (O_reflector A)
    refine (isequiv_adjointify (to (O_reflector A))
             (O_indO (O_reflector A) (fun _ => A) idmap) _ _).
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
(fun x : O_reflector (O_reflector A) =>
 to (O_reflector A)
   (O_indO (O_reflector A)
      (fun _ : O_reflector (O_reflector A) => A) idmap
      x)) == idmap
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
(fun x : O_reflector A =>
 O_indO (O_reflector A)
   (fun _ : O_reflector (O_reflector A) => A) idmap
   (to (O_reflector A) x)) == idmap
    -
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
(fun x : O_reflector (O_reflector A) =>
 to (O_reflector A)
   (O_indO (O_reflector A)
      (fun _ : O_reflector (O_reflector A) => A) idmap
      x)) == idmap intros x; pattern x; apply O_ind_easy.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
x: O_reflector (O_reflector A)
forall oa : O_reflector (O_reflector A),
In_easy
  (to (O_reflector A)
     (O_indO (O_reflector A)
        (fun _ : O_reflector (O_reflector A) => A)
        idmap oa) = oa)
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
x: O_reflector (O_reflector A)
forall a : O_reflector A,
to (O_reflector A)
  (O_indO (O_reflector A)
     (fun _ : O_reflector (O_reflector A) => A) idmap
     (to (O_reflector A) a)) = 
to (O_reflector A) a
      +
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
x: O_reflector (O_reflector A)
forall oa : O_reflector (O_reflector A),
In_easy
  (to (O_reflector A)
     (O_indO (O_reflector A)
        (fun _ : O_reflector (O_reflector A) => A)
        idmap oa) = oa) intros oa; apply inO_pathsO.
      +
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
x: O_reflector (O_reflector A)
forall a : O_reflector A,
to (O_reflector A)
  (O_indO (O_reflector A)
     (fun _ : O_reflector (O_reflector A) => A) idmap
     (to (O_reflector A) a)) = to (O_reflector A) a intros a; apply ap.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
x: O_reflector (O_reflector A)
a: O_reflector A
O_indO (O_reflector A)
  (fun _ : O_reflector (O_reflector A) => A) idmap
  (to (O_reflector A) a) = a
        exact (O_indO_beta (O_reflector A) (fun _ => A) idmap a).
    -
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
(fun x : O_reflector A =>
 O_indO (O_reflector A)
   (fun _ : O_reflector (O_reflector A) => A) idmap
   (to (O_reflector A) x)) == idmap intros a.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
a: O_reflector A
O_indO (O_reflector A)
  (fun _ : O_reflector (O_reflector A) => A) idmap
  (to (O_reflector A) a) = a
      exact (O_indO_beta (O_reflector A) (fun _ => A) idmap a).
  Defined.

  (** It seems to be surprisingly hard to show repleteness (without univalence).  We basically have to manually develop enough functoriality of [O] and naturality of [to O]. *)
  Local Definition inO_equiv_inO_easy (A B : Type)
        (A_inO : In_easy A) (f : A -> B) (feq : IsEquiv f)
    : In_easy B.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
In_easy B
  Proof.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
In_easy B
    simple refine (isequiv_commsq (to A) (to B) f
             (O_ind_easy A (fun _ => O_reflector B) _ (fun a => to B (f a))) _).
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
forall oa : O_reflector A,
In_easy ((fun _ : O_reflector A => O_reflector B) oa)
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
O_ind_easy A (fun _ : O_reflector A => O_reflector B)
  ?B_inO (fun a : A => to B (f a)) o 
to A == to B o f
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
IsEquiv (to A)
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
IsEquiv
  (O_ind_easy A
     (fun _ : O_reflector A => O_reflector B) 
     ?B_inO (fun a : A => to B (f a)))
    -
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
forall oa : O_reflector A,
In_easy ((fun _ : O_reflector A => O_reflector B) oa) intros; apply O_inO_easy.
    -
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
O_ind_easy A (fun _ : O_reflector A => O_reflector B)
  (fun _ : O_reflector A => O_inO_easy B)
  (fun a : A => to B (f a)) o to A == to B o f intros a; exact (O_ind_easy_beta A (fun _ => O_reflector B) _ _ a).
    -
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
IsEquiv (to A) exact A_inO.
    -
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
IsEquiv
  (O_ind_easy A
     (fun _ : O_reflector A => O_reflector B)
     (fun _ : O_reflector A => O_inO_easy B)
     (fun a : A => to B (f a))) simple refine (isequiv_adjointify _
               (O_ind_easy B (fun _ => O_reflector A) _ (fun b => to A (f^-1 b))) _ _);
        intros x.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x: O_reflector B
In_easy ((fun _ : O_reflector B => O_reflector A) x)
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x: O_reflector B
O_ind_easy A (fun _ : O_reflector A => O_reflector B)
  (fun _ : O_reflector A => O_inO_easy B)
  (fun a : A => to B (f a))
  (O_ind_easy B
     (fun _ : O_reflector B => O_reflector A)
     (fun x : O_reflector B => ?Goal)
     (fun b : B => to A (f^-1 b)) x) = x
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x: O_reflector A
O_ind_easy B (fun _ : O_reflector B => O_reflector A)
  (fun x : O_reflector B => ?Goal)
  (fun b : B => to A (f^-1 b))
  (O_ind_easy A
     (fun _ : O_reflector A => O_reflector B)
     (fun _ : O_reflector A => O_inO_easy B)
     (fun a : A => to B (f a)) x) = x
      +
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x: O_reflector B
In_easy ((fun _ : O_reflector B => O_reflector A) x) apply O_inO_easy.
      +
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x: O_reflector B
O_ind_easy A (fun _ : O_reflector A => O_reflector B)
  (fun _ : O_reflector A => O_inO_easy B)
  (fun a : A => to B (f a))
  (O_ind_easy B
     (fun _ : O_reflector B => O_reflector A)
     (fun _ : O_reflector B => O_inO_easy A)
     (fun b : B => to A (f^-1 b)) x) = x pattern x; refine (O_ind_easy B _ _ _ x); intros.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x, oa: O_reflector B
In_easy
  (O_ind_easy A
     (fun _ : O_reflector A => O_reflector B)
     (fun _ : O_reflector A => O_inO_easy B)
     (fun a : A => to B (f a))
     (O_ind_easy B
        (fun _ : O_reflector B => O_reflector A)
        (fun _ : O_reflector B => O_inO_easy A)
        (fun b : B => to A (f^-1 b)) oa) = oa)
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x: O_reflector B
a: B
O_ind_easy A (fun _ : O_reflector A => O_reflector B)
  (fun _ : O_reflector A => O_inO_easy B)
  (fun a : A => to B (f a))
  (O_ind_easy B
     (fun _ : O_reflector B => O_reflector A)
     (fun _ : O_reflector B => O_inO_easy A)
     (fun b : B => to A (f^-1 b)) 
     (to B a)) = to B a
        *
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x, oa: O_reflector B
In_easy
  (O_ind_easy A
     (fun _ : O_reflector A => O_reflector B)
     (fun _ : O_reflector A => O_inO_easy B)
     (fun a : A => to B (f a))
     (O_ind_easy B
        (fun _ : O_reflector B => O_reflector A)
        (fun _ : O_reflector B => O_inO_easy A)
        (fun b : B => to A (f^-1 b)) oa) = oa) apply inO_pathsO.
        *
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x: O_reflector B
a: B
O_ind_easy A (fun _ : O_reflector A => O_reflector B)
  (fun _ : O_reflector A => O_inO_easy B)
  (fun a : A => to B (f a))
  (O_ind_easy B
     (fun _ : O_reflector B => O_reflector A)
     (fun _ : O_reflector B => O_inO_easy A)
     (fun b : B => to A (f^-1 b)) (to B a)) = to B a simpl; abstract (repeat rewrite O_ind_easy_beta; apply ap, eisretr).
      +
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x: O_reflector A
O_ind_easy B (fun _ : O_reflector B => O_reflector A)
  (fun _ : O_reflector B => O_inO_easy A)
  (fun b : B => to A (f^-1 b))
  (O_ind_easy A
     (fun _ : O_reflector A => O_reflector B)
     (fun _ : O_reflector A => O_inO_easy B)
     (fun a : A => to B (f a)) x) = x pattern x; refine (O_ind_easy A _ _ _ x); intros.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x, oa: O_reflector A
In_easy
  (O_ind_easy B
     (fun _ : O_reflector B => O_reflector A)
     (fun _ : O_reflector B => O_inO_easy A)
     (fun b : B => to A (f^-1 b))
     (O_ind_easy A
        (fun _ : O_reflector A => O_reflector B)
        (fun _ : O_reflector A => O_inO_easy B)
        (fun a : A => to B (f a)) oa) = oa)
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x: O_reflector A
a: A
O_ind_easy B (fun _ : O_reflector B => O_reflector A)
  (fun _ : O_reflector B => O_inO_easy A)
  (fun b : B => to A (f^-1 b))
  (O_ind_easy A
     (fun _ : O_reflector A => O_reflector B)
     (fun _ : O_reflector A => O_inO_easy B)
     (fun a : A => to B (f a)) 
     (to A a)) = to A a
        *
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x, oa: O_reflector A
In_easy
  (O_ind_easy B
     (fun _ : O_reflector B => O_reflector A)
     (fun _ : O_reflector B => O_inO_easy A)
     (fun b : B => to A (f^-1 b))
     (O_ind_easy A
        (fun _ : O_reflector A => O_reflector B)
        (fun _ : O_reflector A => O_inO_easy B)
        (fun a : A => to B (f a)) oa) = oa) apply inO_pathsO.
        *
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A, B: Type
A_inO: In_easy A
f: A -> B
feq: IsEquiv f
x: O_reflector A
a: A
O_ind_easy B (fun _ : O_reflector B => O_reflector A)
  (fun _ : O_reflector B => O_inO_easy A)
  (fun b : B => to A (f^-1 b))
  (O_ind_easy A
     (fun _ : O_reflector A => O_reflector B)
     (fun _ : O_reflector A => O_inO_easy B)
     (fun a : A => to B (f a)) (to A a)) = to A a simpl; abstract (repeat rewrite O_ind_easy_beta; apply ap, eissect).
  Defined.

  Local Definition inO_paths_easy (A : Type) (A_inO : In_easy A) (a a' : A)
    : In_easy (a = a').
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
A_inO: In_easy A
a, a': A
In_easy (a = a')
  Proof.
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
A_inO: In_easy A
a, a': A
In_easy (a = a')
    simple refine (inO_equiv_inO_easy (to A a = to A a') _ _
                                      (@ap _ _ (to A) a a')^-1 _).
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
A_inO: In_easy A
a, a': A
In_easy (to A a = to A a')
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
A_inO: In_easy A
a, a': A
IsEquiv (ap (to A))
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
A_inO: In_easy A
a, a': A
IsEquiv (ap (to A))^-1
    -
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
A_inO: In_easy A
a, a': A
In_easy (to A a = to A a') apply inO_pathsO.
    -
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
A_inO: In_easy A
a, a': A
IsEquiv (ap (to A)) exact (@isequiv_ap _ _ _ A_inO _ _).
    -
O_reflector: Type -> Type
to: forall T : Type, T -> O_reflector T
O_indO: forall (A : Type)
(B : O_reflector A -> Type),
(forall a : A, O_reflector (B (to A a))) ->
forall z : O_reflector A, O_reflector (B z)
O_indO_beta: forall (A : Type)
(B : O_reflector A -> Type)
(f : forall a : A,
     O_reflector (B (to A a))) 
(a : A), O_indO A B f (to A a) = f a
inO_pathsO: forall (A : Type) (z z' : O_reflector A),
IsEquiv (to (z = z'))
A: Type
A_inO: In_easy A
a, a': A
IsEquiv (ap (to A))^-1 apply isequiv_inverse.
  Defined.

  Definition easy_modality : Modality
    := Build_Modality In_easy _ inO_equiv_inO_easy O_reflector O_inO_easy to O_ind_easy O_ind_easy_beta inO_paths_easy.

End EasyModalities.


(** ** The modal factorization system *)

Section ModalFact.
  Context `{fs : Funext} (O : Modality).

  (** Lemma 7.6.4 *)
  Definition image {A B : Type} (f : A -> B)
  : Factorization (@IsConnMap O) (@MapIn O) f.
fs: Funext
O: Modality
A, B: Type
f: A -> B
Factorization (@IsConnMap O) (@MapIn O) f
  Proof.
fs: Funext
O: Modality
A, B: Type
f: A -> B
Factorization (@IsConnMap O) (@MapIn O) f
    pose mapinO_pr1. (** Slightly speeds up next line. *)
fs: Funext
O: Modality
A, B: Type
f: A -> B
m:= mapinO_pr1: forall (O : Subuniverse) (A : Type)
(B : A -> Type),
(forall a : A, In O (B a)) -> MapIn O pr1
Factorization (@IsConnMap O) (@MapIn O) f
    refine (Build_Factorization {b : B & O (hfiber f b)}
                                (fun a => (f a ; to O _ (a;1)))
                                pr1
                                (fun a => 1)
                                _ _).
fs: Funext
O: Modality
A, B: Type
f: A -> B
m:= mapinO_pr1: forall (O : Subuniverse) (A : Type)
(B : A -> Type),
(forall a : A, In O (B a)) -> MapIn O pr1
IsConnMap O
  (fun a : A => (f a; to O (hfiber f (f a)) (a; 1)))
    pose conn_map_functor_sigma. (** Slightly speeds up next line. *)
fs: Funext
O: Modality
A, B: Type
f: A -> B
m:= mapinO_pr1: forall (O : Subuniverse) (A : Type)
(B : A -> Type),
(forall a : A, In O (B a)) -> MapIn O pr1
i:= conn_map_functor_sigma: forall (O : ReflectiveSubuniverse) (A B : Type)
(P : A -> Type) (Q : B -> Type) (f : A -> B)
(g : forall a : A, P a -> Q (f a)),
(forall a : A, IsConnMap O (g a)) ->
IsConnMap O f -> IsConnMap O (functor_sigma f g)
IsConnMap O
  (fun a : A => (f a; to O (hfiber f (f a)) (a; 1)))
    exact (conn_map_compose O
              (equiv_fibration_replacement f)
              (functor_sigma idmap (fun b => to O (hfiber f b)))).
  Defined.

  #[export] Instance conn_map_factor1_image {A B : Type} (f : A -> B)
  : IsConnMap O (factor1 (image f))
    := inclass1 (image f).

  #[export] Instance inO_map_factor2_image {A B : Type} (f : A -> B)
  : MapIn O (factor2 (image f))
    := inclass2 (image f).

  (** This is the composite of the three displayed equivalences at the beginning of the proof of Lemma 7.6.5.  Note that it involves only a single factorization of [f]. *)
  Lemma O_hfiber_O_fact {A B : Type} {f : A -> B}
        (fact : Factorization (@IsConnMap O) (@MapIn O) f) (b : B)
  : O (hfiber (factor2 fact o factor1 fact) b)
      <~> hfiber (factor2 fact) b.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
b: B
O (hfiber (factor2 fact o factor1 fact) b) <~>
hfiber (factor2 fact) b
  Proof.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
b: B
O (hfiber (factor2 fact o factor1 fact) b) <~>
hfiber (factor2 fact) b
    refine (_ oE
             (equiv_O_functor O
               (hfiber_compose (factor1 fact) (factor2 fact) b))).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
b: B
O
  {w : hfiber (factor2 fact) b &
  hfiber (factor1 fact) w.1} <~>
hfiber (factor2 fact) b
    nrefine (equiv_sigma_contr (fun w => O (hfiber (factor1 fact) w.1)) oE _).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
b: B
forall a : {x : fact & factor2 fact x = b},
Contr (O (hfiber (factor1 fact) a.1))
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
b: B
O
  {w : hfiber (factor2 fact) b &
  hfiber (factor1 fact) w.1} <~>
{w : {x : fact & factor2 fact x = b} &
O (hfiber (factor1 fact) w.1)}
    -
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
b: B
forall a : {x : fact & factor2 fact x = b},
Contr (O (hfiber (factor1 fact) a.1)) intros w; exact (inclass1 fact w.1).
    -
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
b: B
O
  {w : hfiber (factor2 fact) b &
  hfiber (factor1 fact) w.1} <~>
{w : {x : fact & factor2 fact x = b} &
O (hfiber (factor1 fact) w.1)} nrefine ((equiv_sigma_inO_O (fun w => hfiber (factor1 fact) w.1))^-1)%equiv.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
b: B
In O {x : fact & factor2 fact x = b}
      exact (inclass2 fact b).
  Defined.

  (** This is the corresponding first three of the displayed "mapsto"s in proof of Lemma 7.6.5, and also the last three in reverse order, generalized to an arbitrary path [p].  Note that it is much harder to prove than in the book, because we are working in the extra generality of a modality where [O_ind_beta] is only propositional. *)
  Lemma O_hfiber_O_fact_inverse_beta {A B : Type} {f : A -> B}
        (fact : Factorization (@IsConnMap O) (@MapIn O) f)
        (a : A) (b : B) (p : factor2 fact (factor1 fact a) = b)
  : (O_hfiber_O_fact fact b)^-1
      (factor1 fact a ; p) = to O _ (a ; p).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
(O_hfiber_O_fact fact b)^-1 (factor1 fact a; p) =
to O (hfiber (factor2 fact o factor1 fact) b) (a; p)
  Proof.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
(O_hfiber_O_fact fact b)^-1 (factor1 fact a; p) =
to O (hfiber (factor2 fact o factor1 fact) b) (a; p)
    set (g := factor1 fact); set (h := factor2 fact).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
(O_hfiber_O_fact fact b)^-1 (g a; p) =
to O (hfiber (h o g) b) (a; p)
    apply moveR_equiv_V.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
(g a; p) =
O_hfiber_O_fact fact b
  (to O (hfiber (fun x : A => h (g x)) b) (a; p))
    unfold O_hfiber_O_fact.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
(g a; p) =
(equiv_sigma_contr
   (fun w : {x : fact & factor2 fact x = b} =>
    O (hfiber (factor1 fact) w.1))
 oE (equiv_sigma_inO_O
       (fun w : {x : fact & factor2 fact x = b} =>
        hfiber (factor1 fact) w.1))^-1
 oE equiv_O_functor O
      (hfiber_compose (factor1 fact) (factor2 fact) b))
  (to O (hfiber (fun x : A => h (g x)) b) (a; p))
    ev_equiv.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
(g a; p) =
equiv_sigma_contr
  (fun w : {x : fact & factor2 fact x = b} =>
   O (hfiber (factor1 fact) w.1))
  ((equiv_sigma_inO_O
      (fun w : {x : fact & factor2 fact x = b} =>
       hfiber (factor1 fact) w.1))^-1
     (equiv_O_functor O
        (hfiber_compose (factor1 fact) (factor2 fact)
           b)
        (to O (hfiber (fun x : A => h (g x)) b) (a; p))))
    apply moveL_equiv_M.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
(equiv_sigma_contr
   (fun w : {x : fact & factor2 fact x = b} =>
    O (hfiber (factor1 fact) w.1)))^-1 (g a; p) =
(equiv_sigma_inO_O
   (fun w : {x : fact & factor2 fact x = b} =>
    hfiber (factor1 fact) w.1))^-1
  (equiv_O_functor O
     (hfiber_compose (factor1 fact) (factor2 fact) b)
     (to O (hfiber (fun x : A => h (g x)) b) (a; p)))
    transitivity (exist (fun (w : hfiber h b) => O (hfiber g w.1))
                         (g a; p) (to O (hfiber g (g a)) (a ; 1))).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
(equiv_sigma_contr
   (fun w : {x : fact & factor2 fact x = b} =>
    O (hfiber (factor1 fact) w.1)))^-1 (g a; p) =
((g a; p); to O (hfiber g (g a; p).1) (a; 1))
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
((g a; p); to O (hfiber g (g a; p).1) (a; 1)) =
(equiv_sigma_inO_O
   (fun w : {x : fact & factor2 fact x = b} =>
    hfiber (factor1 fact) w.1))^-1
  (equiv_O_functor O
     (hfiber_compose (factor1 fact) (factor2 fact) b)
     (to O (hfiber (fun x : A => h (g x)) b) (a; p)))
    -
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
(equiv_sigma_contr
   (fun w : {x : fact & factor2 fact x = b} =>
    O (hfiber (factor1 fact) w.1)))^-1 (g a; p) =
((g a; p); to O (hfiber g (g a; p).1) (a; 1)) apply moveR_equiv_V; reflexivity.
    -
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
((g a; p); to O (hfiber g (g a; p).1) (a; 1)) =
(equiv_sigma_inO_O
   (fun w : {x : fact & factor2 fact x = b} =>
    hfiber (factor1 fact) w.1))^-1
  (equiv_O_functor O
     (hfiber_compose (factor1 fact) (factor2 fact) b)
     (to O (hfiber (fun x : A => h (g x)) b) (a; p))) apply moveL_equiv_V.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
equiv_sigma_inO_O
  (fun w : {x : fact & factor2 fact x = b} =>
   hfiber (factor1 fact) w.1)
  ((g a; p); to O (hfiber g (g a; p).1) (a; 1)) =
equiv_O_functor O
  (hfiber_compose (factor1 fact) (factor2 fact) b)
  (to O (hfiber (fun x : A => h (g x)) b) (a; p))
      transitivity (to O _ (exist (fun (w : hfiber h b) => (hfiber g w.1))
                         (g a; p) (a ; 1))).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
equiv_sigma_inO_O
  (fun w : {x : fact & factor2 fact x = b} =>
   hfiber (factor1 fact) w.1)
  ((g a; p); to O (hfiber g (g a; p).1) (a; 1)) =
to O {w : hfiber h b & hfiber g w.1} ((g a; p); a; 1)
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
to O {w : hfiber h b & hfiber g w.1} ((g a; p); a; 1) =
equiv_O_functor O
  (hfiber_compose (factor1 fact) (factor2 fact) b)
  (to O (hfiber (fun x : A => h (g x)) b) (a; p))
      +
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
equiv_sigma_inO_O
  (fun w : {x : fact & factor2 fact x = b} =>
   hfiber (factor1 fact) w.1)
  ((g a; p); to O (hfiber g (g a; p).1) (a; 1)) =
to O {w : hfiber h b & hfiber g w.1} ((g a; p); a; 1) cbn; repeat rewrite O_rec_beta; reflexivity.
      +
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact: Factorization (@IsConnMap O) (@MapIn O) f
a: A
b: B
p: factor2 fact (factor1 fact a) = b
g:= factor1 fact: A -> fact
h:= factor2 fact: fact -> B
to O {w : hfiber h b & hfiber g w.1} ((g a; p); a; 1) =
equiv_O_functor O
  (hfiber_compose (factor1 fact) (factor2 fact) b)
  (to O (hfiber (fun x : A => h (g x)) b) (a; p)) destruct p; symmetry; apply to_O_natural.
  Qed.

  Section TwoFactorizations.
    Context {A B : Type} (f : A -> B)
            (fact fact' : Factorization (@IsConnMap O) (@MapIn O) f).

    Let H := fun x => fact_factors fact x @ (fact_factors fact' x)^.

    (** Lemma 7.6.5, part 1. *)
    Definition equiv_O_factor_hfibers (b:B)
    : hfiber (factor2 fact) b <~> hfiber (factor2 fact') b.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
b: B
hfiber (factor2 fact) b <~> hfiber (factor2 fact') b
    Proof.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
b: B
hfiber (factor2 fact) b <~> hfiber (factor2 fact') b
      refine (O_hfiber_O_fact fact' b oE _).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
b: B
hfiber (factor2 fact) b <~>
O
  (hfiber
     (fun x : A => factor2 fact' (factor1 fact' x)) b)
      refine (_ oE (O_hfiber_O_fact fact b)^-1).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
b: B
O
  (hfiber (fun x : A => factor2 fact (factor1 fact x))
     b) <~>
O
  (hfiber
     (fun x : A => factor2 fact' (factor1 fact' x)) b)
      apply equiv_O_functor.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
b: B
hfiber (fun x : A => factor2 fact (factor1 fact x)) b <~>
hfiber (fun x : A => factor2 fact' (factor1 fact' x))
  b
      apply equiv_hfiber_homotopic.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
b: B
(fun x : A => factor2 fact (factor1 fact x)) ==
(fun x : A => factor2 fact' (factor1 fact' x))
      exact H.
    Defined.

    (** Lemma 7.6.5, part 2. *)
    Definition equiv_O_factor_hfibers_beta (a : A)
    : equiv_O_factor_hfibers (factor2 fact (factor1 fact a))
                             (factor1 fact a ; 1)
      = (factor1 fact' a ; (H a)^).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
equiv_O_factor_hfibers (factor2 fact (factor1 fact a))
  (factor1 fact a; 1) = (factor1 fact' a; (H a)^)
    Proof.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
equiv_O_factor_hfibers (factor2 fact (factor1 fact a))
  (factor1 fact a; 1) = (factor1 fact' a; (H a)^)
      unfold equiv_O_factor_hfibers.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
(O_hfiber_O_fact fact' (factor2 fact (factor1 fact a))
 oE (equiv_O_functor O
       (equiv_hfiber_homotopic
          (fun x : A => factor2 fact (factor1 fact x))
          (fun x : A =>
           factor2 fact' (factor1 fact' x)) H
          (factor2 fact (factor1 fact a)))
     oE (O_hfiber_O_fact fact
           (factor2 fact (factor1 fact a)))^-1))
  (factor1 fact a; 1) = (factor1 fact' a; (H a)^)
      ev_equiv.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
O_hfiber_O_fact fact' (factor2 fact (factor1 fact a))
  (equiv_O_functor O
     (equiv_hfiber_homotopic
        (fun x : A => factor2 fact (factor1 fact x))
        (fun x : A => factor2 fact' (factor1 fact' x))
        H (factor2 fact (factor1 fact a)))
     ((O_hfiber_O_fact fact
         (factor2 fact (factor1 fact a)))^-1
        (factor1 fact a; 1))) =
(factor1 fact' a; (H a)^)
      apply moveR_equiv_M.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
equiv_O_functor O
  (equiv_hfiber_homotopic
     (fun x : A => factor2 fact (factor1 fact x))
     (fun x : A => factor2 fact' (factor1 fact' x)) H
     (factor2 fact (factor1 fact a)))
  ((O_hfiber_O_fact fact
      (factor2 fact (factor1 fact a)))^-1
     (factor1 fact a; 1)) =
(O_hfiber_O_fact fact' (factor2 fact (factor1 fact a)))^-1
  (factor1 fact' a; (H a)^)
      do 2 rewrite O_hfiber_O_fact_inverse_beta.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
equiv_O_functor O
  (equiv_hfiber_homotopic
     (fun x : A => factor2 fact (factor1 fact x))
     (fun x : A => factor2 fact' (factor1 fact' x)) H
     (factor2 fact (factor1 fact a)))
  (to O
     (hfiber
        (fun x : A => factor2 fact (factor1 fact x))
        (factor2 fact (factor1 fact a))) (a; 1)) =
to O
  (hfiber
     (fun x : A => factor2 fact' (factor1 fact' x))
     (factor2 fact (factor1 fact a))) (a; (H a)^)
      unfold equiv_fun, equiv_O_functor.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
O_functor O
  (equiv_hfiber_homotopic
     (fun x : A => factor2 fact (factor1 fact x))
     (fun x : A => factor2 fact' (factor1 fact' x)) H
     (factor2 fact (factor1 fact a)))
  (to O
     (hfiber
        (fun x : A => factor2 fact (factor1 fact x))
        (factor2 fact (factor1 fact a))) (a; 1)) =
to O
  (hfiber
     (fun x : A => factor2 fact' (factor1 fact' x))
     (factor2 fact (factor1 fact a))) (a; (H a)^)
      transitivity (to O _
                       (equiv_hfiber_homotopic
                          (factor2 fact o factor1 fact)
                          (factor2 fact' o factor1 fact') H
                          (factor2 fact (factor1 fact a)) (a;1))).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
O_functor O
  (equiv_hfiber_homotopic
     (fun x : A => factor2 fact (factor1 fact x))
     (fun x : A => factor2 fact' (factor1 fact' x)) H
     (factor2 fact (factor1 fact a)))
  (to O
     (hfiber
        (fun x : A => factor2 fact (factor1 fact x))
        (factor2 fact (factor1 fact a))) (a; 1)) =
to O
  (hfiber
     (fun x : A => factor2 fact' (factor1 fact' x))
     (factor2 fact (factor1 fact a)))
  (equiv_hfiber_homotopic
     (factor2 fact o factor1 fact)
     (factor2 fact' o factor1 fact') H
     (factor2 fact (factor1 fact a)) (a; 1))
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
to O
  (hfiber
     (fun x : A => factor2 fact' (factor1 fact' x))
     (factor2 fact (factor1 fact a)))
  (equiv_hfiber_homotopic
     (factor2 fact o factor1 fact)
     (factor2 fact' o factor1 fact') H
     (factor2 fact (factor1 fact a)) 
     (a; 1)) =
to O
  (hfiber
     (fun x : A => factor2 fact' (factor1 fact' x))
     (factor2 fact (factor1 fact a))) 
  (a; (H a)^)
      -
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
O_functor O
  (equiv_hfiber_homotopic
     (fun x : A => factor2 fact (factor1 fact x))
     (fun x : A => factor2 fact' (factor1 fact' x)) H
     (factor2 fact (factor1 fact a)))
  (to O
     (hfiber
        (fun x : A => factor2 fact (factor1 fact x))
        (factor2 fact (factor1 fact a))) (a; 1)) =
to O
  (hfiber
     (fun x : A => factor2 fact' (factor1 fact' x))
     (factor2 fact (factor1 fact a)))
  (equiv_hfiber_homotopic
     (factor2 fact o factor1 fact)
     (factor2 fact' o factor1 fact') H
     (factor2 fact (factor1 fact a)) (a; 1)) exact (to_O_natural O _ _).
      -
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
to O
  (hfiber
     (fun x : A => factor2 fact' (factor1 fact' x))
     (factor2 fact (factor1 fact a)))
  (equiv_hfiber_homotopic
     (factor2 fact o factor1 fact)
     (factor2 fact' o factor1 fact') H
     (factor2 fact (factor1 fact a)) (a; 1)) =
to O
  (hfiber
     (fun x : A => factor2 fact' (factor1 fact' x))
     (factor2 fact (factor1 fact a))) (a; (H a)^) apply ap.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
equiv_hfiber_homotopic
  (fun x : A => factor2 fact (factor1 fact x))
  (fun x : A => factor2 fact' (factor1 fact' x)) H
  (factor2 fact (factor1 fact a)) (a; 1) = (a; (H a)^)
        simpl.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
H:= fun x : A =>
fact_factors fact x @ (fact_factors fact' x)^: forall x : A,
factor2 fact (factor1 fact x) =
factor2 fact' (factor1 fact' x)
a: A
(a; (H a)^ @ 1) = (a; (H a)^)
        apply ap; auto with path_hints.
    Qed.

  End TwoFactorizations.

  (** Theorem 7.6.6.  Recall that a lot of hard work was done in [Factorization.path_factorization]. *)
  Definition O_factsys : FactorizationSystem.
fs: Funext
O: Modality
FactorizationSystem
  Proof.
fs: Funext
O: Modality
FactorizationSystem
    refine (Build_FactorizationSystem
              (@IsConnMap O) _ _ _
              (@MapIn O) _ _ _
              (@image) _).
fs: Funext
O: Modality
forall (X Y : Type) (f : X -> Y)
(fact
 fact' : Factorization (@IsConnMap O) (@MapIn O) f),
PathFactorization fact fact'
    intros A B f fact fact'.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
PathFactorization fact fact'
    simple refine (Build_PathFactorization fact fact' _ _ _ _).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
fact <~> fact'
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
?path_intermediate o factor1 fact == factor1 fact'
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
factor2 fact == factor2 fact' o ?path_intermediate
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
forall a : A,
(?path_factor2 (factor1 fact a) @
 ap (factor2 fact') (?path_factor1 a)) @
fact_factors fact' a = fact_factors fact a
    -
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
fact <~> fact' refine (_ oE equiv_fibration_replacement (factor2 fact)).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
{y : B & hfiber (factor2 fact) y} <~> fact'
      refine ((equiv_fibration_replacement (factor2 fact'))^-1 oE _).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
{y : B & hfiber (factor2 fact) y} <~>
{y : B & hfiber (factor2 fact') y}
      apply equiv_functor_sigma_id; intros b; simpl.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
b: B
hfiber (factor2 fact) b <~> hfiber (factor2 fact') b
      apply equiv_O_factor_hfibers.
    -
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
(equiv_fibration_replacement (factor2 fact'))^-1
oE equiv_functor_sigma_id
     (fun b : B =>
      equiv_O_factor_hfibers f fact fact' b
      :
      hfiber (factor2 fact) b <~>
      hfiber (factor2 fact') b)
oE equiv_fibration_replacement (factor2 fact)
o factor1 fact == factor1 fact' intros a; exact (pr1_path (equiv_O_factor_hfibers_beta f fact fact' a)).
    -
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
factor2 fact ==
factor2 fact'
o ((equiv_fibration_replacement (factor2 fact'))^-1
   oE equiv_functor_sigma_id
        (fun b : B =>
         equiv_O_factor_hfibers f fact fact' b
         :
         hfiber (factor2 fact) b <~>
         hfiber (factor2 fact') b)
   oE equiv_fibration_replacement (factor2 fact)) intros x.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
x: fact
factor2 fact x =
factor2 fact'
  (((equiv_fibration_replacement (factor2 fact'))^-1
    oE equiv_functor_sigma_id
         (fun b : B =>
          equiv_O_factor_hfibers f fact fact' b)
    oE equiv_fibration_replacement (factor2 fact)) x)
      exact ((equiv_O_factor_hfibers f fact fact' (factor2 fact x) (x ; 1)).2 ^).
    -
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
forall a : A,
(((fun x : fact =>
   ((equiv_O_factor_hfibers f fact fact'
       (factor2 fact x) (x; 1)).2)^)
  :
  factor2 fact ==
  factor2 fact'
  o ((equiv_fibration_replacement (factor2 fact'))^-1
     oE equiv_functor_sigma_id
          (fun b : B =>
           equiv_O_factor_hfibers f fact fact' b
           :
           hfiber (factor2 fact) b <~>
           hfiber (factor2 fact') b)
     oE equiv_fibration_replacement (factor2 fact)))
   (factor1 fact a) @
 ap (factor2 fact')
   (((fun a0 : A =>
      (equiv_O_factor_hfibers_beta f fact fact' a0)
      ..1)
     :
     (equiv_fibration_replacement (factor2 fact'))^-1
     oE equiv_functor_sigma_id
          (fun b : B =>
           equiv_O_factor_hfibers f fact fact' b
           :
           hfiber (factor2 fact) b <~>
           hfiber (factor2 fact') b)
     oE equiv_fibration_replacement (factor2 fact)
     o factor1 fact == factor1 fact') a)) @
fact_factors fact' a = fact_factors fact a intros a.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
a: A
(((fun x : fact =>
   ((equiv_O_factor_hfibers f fact fact'
       (factor2 fact x) (x; 1)).2)^)
  :
  factor2 fact ==
  factor2 fact'
  o ((equiv_fibration_replacement (factor2 fact'))^-1
     oE equiv_functor_sigma_id
          (fun b : B =>
           equiv_O_factor_hfibers f fact fact' b
           :
           hfiber (factor2 fact) b <~>
           hfiber (factor2 fact') b)
     oE equiv_fibration_replacement (factor2 fact)))
   (factor1 fact a) @
 ap (factor2 fact')
   (((fun a : A =>
      (equiv_O_factor_hfibers_beta f fact fact' a) ..1)
     :
     (equiv_fibration_replacement (factor2 fact'))^-1
     oE equiv_functor_sigma_id
          (fun b : B =>
           equiv_O_factor_hfibers f fact fact' b
           :
           hfiber (factor2 fact) b <~>
           hfiber (factor2 fact') b)
     oE equiv_fibration_replacement (factor2 fact)
     o factor1 fact == factor1 fact') a)) @
fact_factors fact' a = fact_factors fact a
      apply moveR_pM.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
a: A
((equiv_O_factor_hfibers f fact fact'
    (factor2 fact (factor1 fact a))
    (factor1 fact a; 1)).2)^ @
ap (factor2 fact')
  (equiv_O_factor_hfibers_beta f fact fact' a) ..1 =
fact_factors fact a @ (fact_factors fact' a)^
      refine ((inv_V _)^ @ _ @ inv_V _); apply inverse2.
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
a: A
(((equiv_O_factor_hfibers f fact fact'
     (factor2 fact (factor1 fact a))
     (factor1 fact a; 1)).2)^ @
 ap (factor2 fact')
   (equiv_O_factor_hfibers_beta f fact fact' a) ..1)^ =
(fact_factors fact a @ (fact_factors fact' a)^)^
      refine (_ @ pr2_path (equiv_O_factor_hfibers_beta f fact fact' a)).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
a: A
(((equiv_O_factor_hfibers f fact fact'
     (factor2 fact (factor1 fact a))
     (factor1 fact a; 1)).2)^ @
 ap (factor2 fact')
   (equiv_O_factor_hfibers_beta f fact fact' a) ..1)^ =
transport
  (fun x : fact' =>
   factor2 fact' x = factor2 fact (factor1 fact a))
  (equiv_O_factor_hfibers_beta f fact fact' a) ..1
  (equiv_O_factor_hfibers f fact fact'
     (factor2 fact (factor1 fact a))
     (factor1 fact a; 1)).2
      refine (_ @ (transport_paths_Fl _ _)^).
fs: Funext
O: Modality
A, B: Type
f: A -> B
fact, fact': Factorization (@IsConnMap O) (@MapIn O) f
a: A
(((equiv_O_factor_hfibers f fact fact'
     (factor2 fact (factor1 fact a))
     (factor1 fact a; 1)).2)^ @
 ap (factor2 fact')
   (equiv_O_factor_hfibers_beta f fact fact' a) ..1)^ =
(ap (factor2 fact')
   (equiv_O_factor_hfibers_beta f fact fact' a) ..1)^ @
(equiv_O_factor_hfibers f fact fact'
   (factor2 fact (factor1 fact a)) (factor1 fact a; 1)).2
      exact (inv_pp _ _ @ (1 @@ inv_V _)).
  Defined.

End ModalFact.