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