`{Funext} {A : Type} `{IsConnected O A} (C : Type) `{In O C} : IsEquiv (@const A C). Proof. refine (@isequiv_compose _ _ (fun c u => c) _ _ _ (isequiv_ooextendable (fun _ => C) (const_tt A) (ooextendable_const_isconnected_inO A C))). 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.