{A B C D} {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D} `{IsEquiv A C h} `{IsEquiv B D k} (p : k o f == g o h) (b : B) : IsEquiv (functor_hfiber p b) := _.
Require Import Basics Types Diagrams.CommutativeSquares HSet.