proposition: Lemma pbloop_natural (G K : Group) (f : G $-> K) : fmap loops (fmap B f) o* pbloop ==* pbloop o* f.
proof: Proof. srapply phomotopy_homotopy_hset. apply bloop_natural. Defined.
imports: Basics Types Pointed Cubical WildCat Algebra.AbGroups Homotopy.HSpace.Core TruncType Truncations.Core Truncations.Connectedness Homotopy.HomotopyGroup Homotopy.WhiteheadsPrinciple