{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) (c : C) (q : g c = k b) : hfiber (functor_hfiber p b) (c;q) <~> hfiber (functor_hfiber (fun x => (p x)^) c) (b;q^). Proof. rapply (equiv_functor_sigma_id _ oE _ oE (equiv_functor_sigma_id _)^-1). 1,3:intros; rapply equiv_path_sigma. refine (equiv_sigma_assoc _ _ oE _ oE (equiv_sigma_assoc _ _)^-1). apply equiv_functor_sigma_id; intros a; cbn. refine (equiv_sigma_symm _ oE _). do 2 (apply equiv_functor_sigma_id; intro). refine ((equiv_ap inverse _ _)^-1 oE _). refine (equiv_concat_r (inv_V q)^ _ oE _). apply equiv_concat_l. abstract (rewrite !transport_paths_Fl, !inv_pp, !inv_V, concat_pp_p; reflexivity). Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.