{G H} (phi : ooGroupHom G H) : phi 1 = 1. Proof. grouphom_reduce. reflexivity. 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.