Definition maponpaths_12 {Y X A : UU} (f : Y -> X -> A) {y y'} (e_y : y = y') {x x'} (e_x : x = x') : f y x = f y' x' := maponpaths_1 _ e_x @ maponpaths_2 f e_y _.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.