{A B : Type} {f : A -> B} {y : B} (x1 x2 : hfiber f y) : { q : x1.1 = x2.1 & x1.2 = ap f q @ x2.2 } <~> (x1 = x2). Proof. refine (equiv_path_sigma _ _ _ oE _). apply equiv_functor_sigma_id. intros p; simpl. refine (_ oE equiv_moveR_Vp _ _ _). exact (equiv_concat_l (transport_paths_Fl _ _) _). Defined.
Require Import Basics Types Diagrams.CommutativeSquares HSet.