feat(category_theory): essential image of a functor (#5352)
Define essential image of a functor as a predicate and use it to re-express essential surjectivity.
Construct the essential image as a subcategory of the target and use it to factorise an arbitrary functor into a fully faithful functor and an essentially surjective functor.
Also shuffles the import hierarchy a little so that essential image can import full subcategories.
