fact: Definition isequiv_from_functor_sigma {A} (P Q : A -> Type) (g : forall a, P a -> Q a) `{!IsEquiv (functor_sigma idmap g)} : forall (a : A), IsEquiv (g a).
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths