(n : trunc_index) (A B : pType) : pTr n (A * B) <~>* pTr n A * pTr n B. Proof. snrapply Build_pEquiv'. 1: nrapply equiv_Trunc_prod_cmp. reflexivity. Defined.
Require Import Basics Types WildCat Truncations