Definition maponpaths_app_homot {X Y₁ Y₂ : UU} {f g : Y₁ → X → Y₂} (p : ∏ (z : Y₁ × X), f (pr1 z) (pr2 z) = g (pr1 z) (pr2 z)) (x : X) (y : Y₁) : maponpaths (λ f, f x) (app_homot p y) = p (y ,, x). Proof. apply (maponpaths_funextsec (f y)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.