English
There is a natural category structure on any preorder: objects are elements, there is a morphism X → Y iff X ≤ Y, and composition is transitive.
Русский
У множества с отношением порядка имеется естественная структура категории: объекты — элементы множества, морфизм X → Y существует тогда и только тогда, когда X ≤ Y; композиция —Transitivity.
LaTeX
$$$\text{SmallCategory}(α) = \text{structure with } \mathrm{Hom}(X,Y) = \{\text{proof of } X \le Y\}.$$$
Lean4
/-- The category structure coming from a preorder. There is a morphism `X ⟶ Y` if and only if `X ≤ Y`.
Because we don't allow morphisms to live in `Prop`,
we have to define `X ⟶ Y` as `ULift (PLift (X ≤ Y))`.
See `CategoryTheory.homOfLE` and `CategoryTheory.leOfHom`. -/
@[stacks 00D3]
instance (priority := 100) smallCategory (α : Type u) [Preorder α] : SmallCategory α
where
Hom U V := ULift (PLift (U ≤ V))
id X := ⟨⟨le_refl X⟩⟩
comp f g := ⟨⟨le_trans _ _ _ f.down.down g.down.down⟩⟩
