`{P : A -> Type} `{Q : B -> Type} (f : A <~> B) (g : forall a, P a <~> Q (f a)) : (forall a, P a) <~> (forall b, Q b) := (equiv_functor_forall' f (fun a => (g a)^-1%equiv))^-1.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids