Lemma hfibertriangle1 {X Y : UU} (f : X -> Y) {y : Y} {xe1 xe2 : hfiber f y} (e : xe1 = xe2) : pr2 xe1 = maponpaths f (maponpaths pr1 e) @ pr2 xe2. Proof. intros. induction e. simpl. apply idpath. Defined.