{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. Proof. apply equiv_functor_sigma_id; intros q. refine (equiv_moveR_Vp _ _ _ oE _). apply equiv_moveR_pM. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Factorization Truncations.Core Truncations.Connectedness HProp. Require Import Pointed.Core Pointed.pEquiv. Require Import WildCat. Require Import Spaces.Nat.Core.