(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. Proof. pose (O := Build_Subuniverse In' hprop_inO' inO_equiv_inO'). simple refine (' O _ _); intros T. - exact (Build_PreReflects O T (O_reflector' T) (O_inO' T) (to' T)). - srapply reflectsD_from_OO_ind. + rapply O_ind'. + rapply O_ind_beta'. + rapply inO_paths'. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.