(O' O : ReflectiveSubuniverse) `{O << O'} (e : forall (A:Type) (g:A->Type_ O), ExtensionAlong (to O' A) (fun _ => Type_ O) g) : O <<< O'. Proof. intros A; unshelve econstructor; intros P' P_inO; pose (P := fun x => (P' x ; P_inO x) : Type_ O). - exact (fun x => ((e A P).1 x).1). - exact (fun x => ((e A P).1 x).2). - intros x. apply equiv_path. exact (((e A P).2 x)..1). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.