{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). Proof. snrapply @functor_sigma. - exact h. - intros a e; exact ((p a)^ @ ap k e). Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.