{G H} (phi : ooGroupHom G H) (g : G) : phi g^ = (phi g)^. Proof. grouphom_reduce. exact (ap_V phi 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.