Commit 2020-12-19 11:05 656b1bb5

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.