Definition maponpaths_naturality {X Y : UU} {f : X -> Y} {x x' x'' : X} {p : x = x'} {q : x' = x''} {p': f x = f x'} {q': f x' = f x''} (r : maponpaths f p = p') (s : maponpaths f q = q') : maponpaths f (p @ q) = p' @ q'. Proof. intros. induction r, s. apply maponpathscomp0. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.