{n : nat} (X Y : pType) : GroupIsomorphism (Pi n.+1 (X * Y)) (grp_prod (Pi n.+1 X) (Pi n.+1 Y)). 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.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.