{A B : pType} (f : A ->* B) : pfiber (fmap loops f) <~>* loops (pfiber f). Proof. srapply Build_pEquiv'. { etransitivity. 2: srapply equiv_path_sigma. simpl; unfold hfiber. srapply equiv_functor_sigma_id. intro p; cbn. refine (_ oE equiv_moveL_Mp _ _ _). refine (_ oE equiv_concat_r (concat_p1 _) _). refine (_ oE equiv_moveL_Vp _ _ _). refine (_ oE equiv_path_inverse _ _). apply equiv_concat_l. apply transport_paths_Fl. } by pointed_reduce. Defined.
Require Import Basics Types WildCat. Require Import HFiber. Require Import Pointed.Core. Require Import Pointed.pEquiv. Require Import Pointed.Loops.