fact: Definition loop_susp_triangle1 (X : pType) : fmap loops (loop_susp_counit X) o* loop_susp_unit (loops X) ==* pmap_idmap.
imports: Basics Types Pointed.Core Pointed.Loops Pointed.pTrunc Pointed.pEquiv Homotopy.Suspension Homotopy.Freudenthal Truncations WildCat