Zulip Chat Archive

Stream: new members

Topic: Finding the category of Sets and functions

Nicolas Rolland (Aug 15 2023 at 14:12):

I would like to look at the definition of Sets and functions as a category in mathlib. Where is it located ? In generale, how can I lookup instances and their definition for a particular typeclass ?

Matthew Ballard (Aug 15 2023 at 14:15):

docs#CategoryTheory.types for types and functions which may be good enough depending on what you are interested in

To find instances, I usually use the docs. For example, docs#CategoryTheory.Category has a little dropdown which you can expand to see category instances.

Last updated: Dec 20 2023 at 11:08 UTC