{G H} (phi : ooGroupHom G H) (g1 g2 g3 : G) : grouphom_pp phi (g1 @ g2) g3 @ whiskerR (grouphom_pp phi g1 g2) (phi g3) @ concat_pp_p (phi g1) (phi g2) (phi g3) = ap phi (concat_pp_p g1 g2 g3) @ grouphom_pp phi g1 (g2 @ g3) @ whiskerL (phi g1) (grouphom_pp phi g2 g3). Proof. grouphom_reduce. Abort. Section Subgroups. Context {G H : ooGroup} (incl : ooGroupHom H G) `{IsEmbedding incl}.
Require Import Basics Types. Require Import Pointed. Require Import Truncations.Core Truncations.Connectedness. Require Import Homotopy.ClassifyingSpace. Require Import Algebra.Groups. Require Import WildCat.