`(A : X -> Type) (B : X -> Type) : ((forall x, A x) * (forall x, B x)) <~> (forall x, A x * B x) := Build_Equiv _ _ (@prod_coind_uncurried X A B) _. Global Instance istrunc_prod `{IsTrunc n A} `{IsTrunc n B} : IsTrunc n (A * B) | 100. Proof. generalize dependent B; generalize dependent A. simple_induction n n IH; simpl; (intros A ? B ?). { apply (Build_Contr _ (center A, center B)). intros z; apply path_prod; apply contr. } apply istrunc_S. intros x y. exact (istrunc_equiv_istrunc _ (equiv_path_prod x y)). Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.