colimits in Cat

Stream: Is there code for X?

[Emily Riehl]

I found a file CategoryTheory.Category.Cat.Limit that proves that the category of categories has all limits (modulo size). Has anyone shown the same for colimits in Cat?

If not, I imagine it would be useful to demonstrate that they are constructed by means of the reflective subcategory inclusion into reflexive directed graphs (which is a presheaf category and thus cocomplete). The Monads directly has a few theorems such as docs#CategoryTheory.hasColimits_of_reflective which show that such subcategories have colimits though doesn't give a definition of them as far as I can tell.

[Adam Topaz]

I'm quite sure we don't have the colimits instance in mathlib yet, and I agree that it's something that should certainly be added!

[Adam Topaz]

BTW, concerning linking things on zulip, the docs linkifier expects the full name of a declaration. I think we also have a file linkifier? Let's try: file#CategoryTheory/Monad/Limits

[Emily Riehl]

Thanks @Adam Topaz. I've spent the last five minutes editing and reediting trying to figure this out :)