{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 := Build_pEquiv _ _ (functor_pfiber p) _.
Require Import Basics Types WildCat. Require Import HFiber. Require Import Pointed.Core. Require Import Pointed.pEquiv. Require Import Pointed.Loops.