Corollary hfibertriangle1inv0' {X Y : UU} (f : X -> Y) {x : X} {xe2: hfiber f (f x)} (e : (x,,idpath (f x)) = xe2) : maponpaths f (! (maponpaths pr1 e)) = pr2 xe2. Proof. intros. intermediate_path (maponpaths f (! (maponpaths pr1 e)) @ idpath (f x)). - apply pathsinv0, pathscomp0rid. - apply hfibertriangle1inv0. Defined.