{A : Type} : (forall (C : Type) `{In O C} (f : A -> C), NullHomotopy f) -> IsConnected O A. Proof. intros H. exact (isconnected_from_elim_to_O (H (O A) (O_inO A) (to O A))). 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.