Definition 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)) (y : Y₁) : f y = g y := funextsec _ _ _ (λ x, p (y ,, x)).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.