forall {G H : Group} (f : GroupHomomorphism G H) (x y : G), f (x * y) = f x * f y := @issemigrouppreserving_grp_homo. #[export] Hint Immediate : group_db. Global Instance isunitpreserving_grp_homo {G H : Group} (f : GroupHomomorphism G H) : IsUnitPreserving f. Proof. unfold IsUnitPreserving. apply (group_cancelL (f mon_unit)). rhs nrapply grp_unit_r. rhs_V rapply (ap _ (monoid_left_id _ mon_unit)). symmetry. nrapply issemigrouppreserving_grp_homo. 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.