{A B C D} {f : A ->* B} {g : C ->* D} {h : A ->* C} {k : B ->* D} (p : k o* f ==* g o* h) : pfiber f ->* pfiber g. Proof. srapply Build_pMap. + cbn. refine (functor_hfiber2 p (point_eq k)). + srapply path_hfiber. - apply point_eq. - refine (concat_pp_p _ _ _ @ _). apply moveR_Vp. apply (point_htpy p)^. Defined.
Require Import Basics Types WildCat. Require Import HFiber. Require Import Pointed.Core. Require Import Pointed.pEquiv. Require Import Pointed.Loops.