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