(O' O : ReflectiveSubuniverse@{u}) `{O_leq@{u u u} O O', O' <= Sep O} {Y X Z : Type} (f : Y -> X) (g : X -> Z) `{IsConnMap O' _ _ (g o f)} `{IsConnMap O _ _ f} : IsConnMap O' g. Proof. apply conn_map_from_extension_elim. intros P P_inO h. exists (conn_map_elim O' (g o f) P (h o f)). nrefine (conn_map_elim O f _ _); [ exact _ | .. ]. - intros x. pose proof (fun z => inO_leq O' (Sep O) (P z) (P_inO z)). exact _. - intros y. apply (conn_map_comp O' (g o f)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.