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, p, q. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.