{A : Type} {P Q : A -> Type} (f : forall a, P a <-> Q a) : (forall a, P a) <-> (forall a, Q a) := (functor_forall idmap (fun a => fst (f a)), functor_forall idmap (fun a => snd (f a))).
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids