{A : Type} `{IsConnected O A} (C : Type) `{In O C} (f : A -> C) : NullHomotopy f. Proof. set (ff := @O_rec O _ _ _ _ _ f). exists (ff (center _)). intros a. symmetry. refine (ap ff (contr (to O _ a)) @ _). apply O_rec_beta. 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.