n {A P Q} (g : forall a : A, P a -> Q a) `{!IsTruncMap n (functor_sigma idmap g)} : forall a, IsTruncMap n (g a). Proof. intros a v. exact (istrunc_equiv_istrunc _ (hfiber_functor_sigma_idmap _ _ _ _ _)). Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.