{X Y Z : pType} (psi : Y ->* Z) (phi : X ->* Y) : grouphom_compose (group_loops_functor psi) (group_loops_functor phi) == group_loops_functor (pmap_compose psi phi). Proof. intros g. unfold grouphom_fun, grouphom_compose. refine (pointed_htpy (fmap_comp loops _ _) g @ _). pose (p := eisretr (loops_group X) g). change (fmap loops (group_loops_functor psi) (fmap loops (group_loops_functor phi) g) = fmap loops (group_loops_functor (pmap_compose psi phi)) g). rewrite <- p. rewrite !loops_functor_group. apply ap. symmetry; rapply (fmap_comp loops). 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.