fact: Definition isconnected_elim {A : Type} `{IsConnected O A} (C : Type) `{In O C} (f : A -> C) : NullHomotopy f.
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout