Definition maponpaths_fun_fun_natl {X Y Z} {g g':X->Y} {f f':Y->Z} (q:homot g g') (p:homot f f') x : maponpaths f (q x) @ p (g' x) = p (g x) @ maponpaths f' (q x). Proof. intros. destruct (q x). simpl. rewrite pathscomp0rid. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.