Definition maponpaths_fun_fun_fun_natl {X Y Z W} {g g':X->Y} (q:homot g g') (h:Y->Z) {f f':Z->W} (p:homot f f') x : maponpaths f (maponpaths h (q x)) @ p (h (g' x)) = p (h (g x)) @ maponpaths f' (maponpaths h (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.