{A B} (f : A ->* B) : fmap loops (pfib f) o* pfiber_fmap_loops f ==* pfib (fmap loops f). Proof. srapply Build_pHomotopy. - intros [u v]. refine (concat_1p _ @ concat_p1 _ @ _). exact (@ap_pr1_path_sigma _ _ (point A; point_eq f) (point A;point_eq f) _ _). - abstract (pointed_reduce_rewrite; reflexivity). Defined.
Require Import Basics Types WildCat. Require Import HFiber. Require Import Pointed.Core. Require Import Pointed.pEquiv. Require Import Pointed.Loops.