{A B : Type} (f g : A -> B) (h : f == g) (b : B) : hfiber f b <~> hfiber g b. Proof. refine (Build_Equiv _ _ (fun fx => (fx.1 ; (h fx.1)^ @ fx.2)) _). refine (isequiv_adjointify _ (fun gx => (gx.1 ; (h gx.1) @ gx.2)) _ _); intros [a p]; simpl; apply ap. - apply concat_V_pp. - apply concat_p_Vp. Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.