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