{X : pType} : grouphom_idmap (group_loops X) == group_loops_functor (Id (A:=pType) _). Proof. intros g. refine (fmap_id loops _ g @ _). rewrite <- (eisretr (loops_group X) g). unfold grouphom_fun, grouphom_idmap. rewrite !loops_functor_group. exact (ap (loops_group X) (fmap_id 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.