conn_map_O_leq@{i1 i2} (O1 : ReflectiveSubuniverse@{i1}) (O2 : ReflectiveSubuniverse@{i2}) `{O_leq@{i1 i2 i1} O1 O2} {A B : Type@{i1}} (f : A -> B) `{IsConnMap O2 A B f} : IsConnMap O1 f. Proof. apply conn_map_from_extension_elim. intros P P_inO g. rapply (extension_conn_map_elim O2). intros b; rapply (inO_leq O1). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.