fact: Definition equiv_functor_forall_pb {A B : Type} {P : A -> Type} (f : B <~> A) : (forall a, P a) <~> (forall b, P (f b)) := equiv_functor_forall' (Q := P o f) f (fun b => equiv_idmap).
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Contractible Basics.Trunc (istrunc_forall)