fact: Definition functor_hfiber2 {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'.
imports: Basics Types Diagrams.CommutativeSquares HSet