Definition maponpaths_app_fun {X Y : UU} {fx gx : (X → Y) × X} (p : fx = gx) : maponpaths (λ (fx : (X → Y) × X), app_fun fx) p = maponpaths (λ z, z (pr2 fx)) (maponpaths dirprod_pr1 p) @ maponpaths (pr1 gx) (maponpaths dirprod_pr2 p). Proof. induction p. apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.