{A : Type} {B : A -> Type} {P : forall a : A, B a -> Type} (f g : forall a b, P a b) : (forall (a : A) (b : B a), f a b = g a b) <~> f = g := (equiv_path_forall f g) oE (equiv_functor_forall_id (fun a => equiv_path_forall (f a) (g a))).
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids