isconnected_O_leq@{i1 i2} (O1 : ReflectiveSubuniverse@{i1}) (O2 : ReflectiveSubuniverse@{i2}) `{O_leq@{i1 i2 i1} O1 O2} (A : Type@{i1}) `{IsConnected O2 A} : IsConnected O1 A. Proof. apply isconnected_from_elim. intros C C1 f. apply (isconnected_elim O2); srapply inO_leq; exact _. 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.