fact: Definition equiv_loops_image `{Univalence} n {A B : pType} (f : A ->* B) : loops ([image n.+1 f, factor1 (image n.+1 f) (point A)]) <~> image n (fmap loops f).
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core