{A B : Type} {f : A -> B} {x1 x2 : A} (p : f x1 = f x2) : hfiber (ap f) p <~> ((x1 ; p) = (x2 ; 1) :> hfiber f (f x2)). Proof. refine (equiv_path_hfiber (x1;p) (x2;1%path) oE _). unfold hfiber; simpl. apply equiv_functor_sigma_id; intros q. refine (_ oE equiv_path_inverse _ _). exact (equiv_concat_r (concat_p1 _)^ _). Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.