fact: Definition loop_susp_counit_natural {X Y : pType} (f : X ->* Y) : f o* loop_susp_counit X ==* loop_susp_counit Y o* fmap psusp (fmap loops f).
imports: Basics Types Pointed.Core Pointed.Loops Pointed.pTrunc Pointed.pEquiv Homotopy.Suspension Homotopy.Freudenthal Truncations WildCat