{G H} (phi : ooGroupHom G H) (g1 g2 : G) : phi (g1 @ g2) = phi g1 @ phi g2. Proof. grouphom_reduce. exact (ap_pp phi g1 g2). Qed.
Require Import Basics Types. Require Import Pointed. Require Import Truncations.Core Truncations.Connectedness. Require Import Homotopy.ClassifyingSpace. Require Import Algebra.Groups. Require Import WildCat.