fact: Definition grouphom_compose {G H K : ooGroup} (psi : ooGroupHom H K) (phi : ooGroupHom G H) : ooGroupHom G K := pmap_compose psi phi.
imports: Basics Types Pointed Truncations.Core Truncations.Connectedness Homotopy.ClassifyingSpace Algebra.Groups WildCat