{A : Type} : NullHomotopy (to O A) -> IsConnected O A. Proof. intros nh. apply (Build_Contr _ (nh .1)). rapply O_indpaths. intros x; symmetry; apply (nh .2). 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.