Definition maponpathscomp0 {X Y : UU} {x1 x2 x3 : X} (f : X -> Y) (e1 : x1 = x2) (e2 : x2 = x3) : maponpaths f (e1 @ e2) = maponpaths f e1 @ maponpaths f e2. Proof. intros. induction e1. induction e2. apply idpath. Defined.