fact: Definition hfiber_fmap_loops {A B : pType} (f : A ->* B) (p : loops B) : {q : loops A & ap f q = (point_eq f @ p) @ (point_eq f)^} <~> hfiber (fmap loops f) p.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core