fact: Definition equiv_const_isconnected_inO `{Funext} {A : Type} `{IsConnected O A} (C : Type) `{In O C} : C <~> (A -> C) := Build_Equiv _ _ const (isequiv_const_isconnected_inO C).
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout