{A} (P Q : A -> Type) (g : forall a, P a -> Q a) `{!IsEquiv (functor_sigma idmap g)} : forall (a : A), IsEquiv (g a). Proof. intros a; apply isequiv_contr_map. apply istruncmap_from_functor_sigma. exact _. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths.