Definition maponpaths_2 {Y X A : UU} (f : Y -> X -> A) {y y'} (e_y : y = y') x : f y x = f y' x := maponpaths (fun y => f y x) e_y.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.