mathlib

aa590397 - feat(category_theory): presheaf is colimit of representables (#4401)

feat(category_theory): presheaf is colimit of representables (#4401) Show every presheaf (on a small category) is a colimit of representables, and some related results. Suggestions for better names more than welcome.