proposition: Lemma grp_iso_pi_prod {n : nat} (X Y : pType) : GroupIsomorphism (Pi n.+1 (X * Y)) (grp_prod (Pi n.+1 X) (Pi n.+1 Y)).
proof: Proof. snrapply Build_GroupIsomorphism. - apply grp_prod_corec. + exact (fmap (Pi n.+1) (@pfst X Y)). + exact (fmap (Pi n.+1) (@psnd X Y)). - exact (equiv_isequiv (pi_prod X Y (n:=n.+1))). Defined.
imports: Basics Types Pointed HSet Modalities.Modality Truncations.Core Truncations.SeparatedTrunc Algebra.AbGroups WildCat