fact: Definition istrunc_loops {n} (A : pType) `{IsTrunc n.+1 A} : IsTrunc n (loops A) := _.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core