`(A : X -> Type) (P : forall x, A x -> Type) : { f : forall x, A x & forall x, P x (f x) } <~> (forall x, sig (P x)) := Build_Equiv _ _ (sig_coind_uncurried P) _. Global Instance istrunc_sigma `{P : A -> Type} `{IsTrunc n A} `{forall a, IsTrunc n (P a)} : IsTrunc n (sig P) | 100. Proof. generalize dependent A. simple_induction' n; simpl; intros A P ac Pc. { apply (Build_Contr _ (center A; center (P (center A)))). intros [a ?]. refine (path_sigma' P (contr a) (path_contr _ _)). } apply istrunc_S. intros u v. refine (istrunc_isequiv_istrunc _ (path_sigma_uncurried P u v)). Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.