{X Y : pType} (f : X ->* Y) : ooGroupHom (group_loops X) (group_loops Y). Proof. simple refine (Build_pMap _ _ _ _); simpl. - intros [x p]. exists (f x). strip_truncations; apply tr. exact (ap f p @ point_eq f). - apply path_sigma_hprop; simpl. apply point_eq. Defined.
Require Import Basics Types. Require Import Pointed. Require Import Truncations.Core Truncations.Connectedness. Require Import Homotopy.ClassifyingSpace. Require Import Algebra.Groups. Require Import WildCat.