fact: Definition conn_map_fiber {A : Type} {P Q : A -> Type} (f : forall a, P a -> Q a) `{IsConnMap O _ _ (functor_sigma idmap f)} : forall a, IsConnMap O (f a).
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout