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