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