{A} (P Q : A -> Type) (g : forall a, P a -> Q a) : IsEquiv (functor_sigma idmap g) <-> forall a, IsEquiv (g a). Proof. split. - apply isequiv_from_functor_sigma. - intro K. apply isequiv_functor_sigma. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths.