Lemma maponpathshomid2 {X : UU} (f : X -> X) (h : ∏ x : X, f x = x) (x x' : X) (e: f x = f x') : maponpaths f (maponpathshomidinv f h _ _ e) = e. Proof. intros. unfold maponpathshomidinv. apply (pathscomp0 (maponpathshomid1 f h (! h x @ e @ h x'))). assert (l : ∏ (X : UU) (a b c d : X) (p : a = b) (q : a = c) (r : c = d), p @ (!p @ q @ r) @ !r = q). { intros. induction p. induction q. induction r. apply idpath. } apply (l _ _ _ _ _ (h x) e (h x')). Defined.