(G H : Group) := Build_GroupHomomorphism { grp_homo_map :> group_type G -> group_type H; issemigrouppreserving_grp_homo :: IsSemiGroupPreserving grp_homo_map; }.
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.