Definition maponpaths_13 {Z Y X A : UU} (f : Z -> Y -> X -> A) {z z'} (e_z : z = z') (y:Y) {x x'} (e_x : x = x') : f z y x = f z' y x' := maponpaths_123 _ e_z (idpath y) e_x.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.