{X Y : pType} (f : X ->* Y) : fmap loops (group_loops_functor f) o loops_group X == loops_group Y o fmap loops f. Proof. intros x. apply (equiv_inj (equiv_path_sigma_hprop _ _)^-1). simpl. unfold pr1_path; rewrite !ap_pp. rewrite ap_V, !ap_pr1_path_sigma_hprop. apply whiskerL, whiskerR. transitivity (ap (fun X0 : {x0 : X & merely (x0 = point X)} => f X0.1) (path_sigma_hprop (point X; tr 1) (point X; tr 1) x)). - match goal with |- ap ?f (ap ?g ?p) = ?z => symmetry; refine (ap_compose g f p) end. - rewrite ap_compose; apply ap. apply ap_pr1_path_sigma_hprop. 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.