{X Y : pType} `{IsTrunc 1 X} `{IsTrunc 1 Y} : (X ->** Y) ->* [LoopGroup X $-> LoopGroup Y, grp_homo_const]. Proof. snrapply Build_pMap. - intro f. snrapply Build_GroupHomomorphism. + exact (fmap loops f). + nrapply fmap_loops_pp. - cbn beta. apply equiv_path_grouphomomorphism. exact (pointed_htpy fmap_loops_pconst). Defined.
Require Import Basics Types. Require Import Pointed WildCat. Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare. Require Import Algebra.AbGroups. Require Import Homotopy.HSpace.Core. Require Import TruncType. Require Import Truncations.Core Truncations.Connectedness. Require Import Homotopy.HomotopyGroup. Require Import Homotopy.WhiteheadsPrinciple. Module Import ClassifyingSpaceNotation.