Accessible functors satisfy the solution set condition

If F : C ⥤ D is an accessible functor between accessible categories, then F satisfies the solution set condition (this is corollary 2.45 in the book by Adámek and Rosický).

References

• Adámek, J. and Rosický, J., Locally presentable and accessible categories

theorem CategoryTheory.SolutionSetCondition.of_isCardinalAccessible {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [IsAccessibleCategory.{w, v_1, u_1} C] [IsAccessibleCategory.{w, v_2, u_2} D] (F : Functor C D) [Functor.IsAccessible.{w, v_1, v_2, u_1, u_2} F] : SolutionSetCondition F

An accessible functor between accessible categories satisfies the solution set condition. This is corollary 2.45 in [AR94].