Lemma hfibertriangle2 {X Y : UU} (f : X -> Y) {y : Y} (xe1 xe2: hfiber f y) (ee: pr1 xe1 = pr1 xe2) (eee: pr2 xe1 = maponpaths f ee @ (pr2 xe2)) : xe1 = xe2. Proof. intros. induction xe1 as [t e1]. induction xe2 as [t' e2]. simpl in *. fold (make_hfiber f t e1). fold (make_hfiber f t' e2). induction ee. simpl in eee. apply (maponpaths (λ e, make_hfiber f t e) eee). Defined.