fact: Definition conn_map_sum {A B A' B'} (f : A -> A') (g : B -> B') `{IsConnMap O _ _ f} `{IsConnMap O _ _ g} : IsConnMap O (functor_sum f g).
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout