Two-object category

Stream: Is there code for X?

[Gareth Ma]

Is the two-object category $\mathbb{2} = (0 \to 1)$ (two objects $0$ and $1$ with an arrow between them) defined in Mathlib/

[Andrew Yang]

Fin 2 (as a preorder)

[Gareth Ma]

Maybe I'm missing some imports, let me try

[Gareth Ma]

Ahha okay thanks, needed import Mathlib.CategoryTheory.FintypeCat

[Andrew Yang]

I think Mathlib/CategoryTheory/Category/Preorder.lean is enough.