{X Y Z: Type} (f g : X -> Y -> Z) : (forall x y, f x y = g x y) <~> f = g. Proof. refine (equiv_path_arrow _ _ oE _). apply equiv_functor_forall_id; intro x. apply equiv_path_arrow. Defined.
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.