the category of sets

Stream: Is there code for X?

[Dean Young]

Is there code for the category of sets? I mean I want a type like this:

def 𝕊𝕖𝕥 : Category Type := by
sorry

so it would have an entry Type as 𝕊𝕖𝕥.α and make use of math lib's categories.

[Kyle Miller]

Yes, Type forms a large category. docs#CategoryTheory.types

(It's also a concrete category, with the forgetful functor being the identity functor. docs#CategoryTheory.ConcreteCategory.types)