(O' O : ReflectiveSubuniverse) `{O << O'} `{IsAccRSU O'} `{In (lift_accrsu O') (Type_ O)} : O <<< O'. Proof. apply O_lex_leq_extendable_TypeO. intros A g. assert (O_inverts (lift_accrsu O') (to O' A)). - rapply (O_inverts_O_leq' (lift_accrsu O') O'). - exact (fst (ooextendable_O_inverts (lift_accrsu O') (to O' A) (Type_ O) 1%nat) g). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.