Group -> Group -> Group. Proof. intros G H. srapply (Build_Group (G * H)). { intros [g1 h1] [g2 h2]. exact (g1 * g2, h1 * h2). } 1: exact (mon_unit, mon_unit). { intros [g h]. exact (-g, -h). } repeat split. 1: exact _. all: grp_auto. 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.