Lemma maponpathshomid1 {X : UU} (f : X -> X) (h: ∏ x : X, f x = x) {x x' : X} (e : x = x') : maponpaths f e = (h x) @ e @ (! h x'). Proof. intros. induction e. simpl. apply pathsinv0. apply pathsinv0r. Defined.