Preorders as categories #
We install a category instance on any preorder. This is not to be confused with the category of
preorders, defined in
We show that monotone functions between preorders correspond to functors of the associated
categories. Furthermore, galois connections correspond to adjoint functors.
Main definitions #
le_of_hom provide translations between inequalities in the preorder, and
morphisms in the associated category.
monotone.functor is the functor associated to a monotone function.
galois_connection.adjunction is the adjunction associated to a galois connection.
Preorder_to_Cat is the functor embedding the category of preorders into
Express an inequality as a morphism in the corresponding preorder category.
Extract the underlying inequality from a morphism in a preorder category.
Construct a morphism in the opposite of a preorder category from an inequality.
A monotone function between preorders induces a functor between the associated categories.
A galois connection between preorders induces an adjunction between the associated categories.
A functor between preorder categories is monotone.
An adjunction between preorder categories induces a galois connection.
A categorical equivalence between partial orders is just an order isomorphism.