(G : ooGroup) : grouphom_idmap G == idmap. Proof. intros g; grouphom_reduce. exact (ap_idmap g). 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.