{A B C D} {f : A ->* B} {g : C ->* D} {h : A ->* C} {k : B ->* D} (p : k o* f ==* g o* h) : h o* pfib f ==* pfib g o* functor_pfiber p. Proof. srapply Build_pHomotopy. - intros x; reflexivity. - apply moveL_pV. cbn; unfold functor_sigma; cbn. abstract (rewrite ap_pr1_path_sigma, concat_p1; reflexivity). Defined.
Require Import Basics Types WildCat. Require Import HFiber. Require Import Pointed.Core. Require Import Pointed.pEquiv. Require Import Pointed.Loops.