{G H} (f : GroupHomomorphism G H) : forall x, f (- x) = -(f x). Proof. intro x. apply (inverse_unique (f x)). + refine (_ @ grp_homo_unit f). refine ((grp_homo_op f (-x) x)^ @ _). apply ap. apply grp_inv_l. + apply grp_inv_r. 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.