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