{n : nat} (X Y : pType) : pPi n (X * Y) <~>* (pPi n X) * (pPi n Y). Proof. snrapply Build_pEquiv. - rapply (equiv_pprod_coind (pfam_const _) (pfam_const _)); split. + exact (fmap (pPi n) (@pfst X Y)). + exact (fmap (pPi n) (@psnd X Y)). - snrapply (isequiv_homotopic' (' X Y)). intro xy. destruct n; strip_truncations. + apply path_prod; reflexivity. + apply path_prod. 1,2: apply (ap tr). * exact (pfst_iterated_loops_prod X Y (n:=n.+1) xy). * exact (psnd_iterated_loops_prod X Y (n:=n.+1) xy). Defined.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.