(Co)limits in a preorder category #
We provide basic results about the nullary and binary (co)products in the associated category of a preordered type.
The least element in a preordered type is initial in the category associated to this preorder.
Instances For
The greatest element of a preordered type is terminal in the category associated to this preorder.
Instances For
The infimum of two elements in a preordered type is a binary product in the category associated to this preorder.
Equations
Instances For
The supremum of two elements in a preordered type is a binary coproduct in the category associated to this preorder.