{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} {b' : D} (q : k b = b') : hfiber f b <~> hfiber g b' := Build_Equiv _ _ (functor_hfiber2 p q) _.
Require Import Basics Types Diagrams.CommutativeSquares HSet.