The category of sets in mathlib

Stream: new members

[Dean Young]

The category of Sets, which would be of type Cat or of type Category (Type.{u}), is a pretty simple thing to make. But I was hoping there would be a standard one already. Is that the case?

[Johan Commelin]

Sure, just treat Type as a category. There is an instance of Category Type that will be picked up automatically

[Dean Young]

Wow thanks Johan.

[Dean Young]

Wait, what if I wanted a functor F : Functor 𝕊𝕖𝕥 𝕊𝕖𝕥. In that case, I would want to be able to name 𝕊𝕖𝕥 : Category Type.{u}.

[Junyan Xu]

Just write F : Functor Type Type (or Functor (Type u) (Type v))
mathlib4 docs doesn't show the notation but you can write F : Type ⥤ Type too.