`{P : A -> Type} `{Q : A -> Type} (g : forall a, P a <~> Q a) : (forall a, P a) <~> (forall a, Q a) := equiv_functor_forall (equiv_idmap A) g.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids