{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* pequiv_pfiber h k p := square_functor_pfiber p.
Require Import Basics Types WildCat. Require Import HFiber. Require Import Pointed.Core. Require Import Pointed.pEquiv. Require Import Pointed.Loops.