{A B C D : Group} : A ≅ B -> C ≅ D -> (grp_prod A C) ≅ (grp_prod B D). Proof. intros f g. srapply Build_GroupIsomorphism'. 1: srapply (equiv_functor_prod (f:=f) (g:=g)). simpl. unfold functor_prod. intros x y. apply path_prod. 1,2: apply grp_homo_op. Defined.
Require Import Basics Types HProp HFiber HSet. Require Import Homotopy.IdentitySystems. Require Import (notations) Classes.interfaces.canonical_names. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Int. Require Import Truncations.Core.