(b : B) : hfiber (hfiber_compose_map (g b)) (b;1) <~> hfiber f b. Proof. unfold hfiber, hfiber_compose_map. refine (_ oE equiv_functor_sigma_id (fun x => (equiv_path_sigma _ _ _)^-1)); cbn. make_equiv_contr_basedpaths. Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.