module Order.Cat where
Posets as categoriesπ
We have already remarked a poset is a special kind of category. This module actually formalises that connection by constructing a fully faithful functor from the category of posets into the category of strict categories. The construction of a category from a poset is entirely unsurprising, but it is lengthy, thus ending up in this module.
posetβcategory : β {β ββ²} β Posets.Ob β Precategory β ββ² posetβcategory P = cat module poset-to-category where module P = Poset P open Precategory cat : Precategory _ _ cat .Ob = P.Ob cat .Hom = P._β€_ cat .id = P.β€-refl cat ._β_ f g = P.β€-trans g f cat .idr f = P.β€-thin _ _ cat .idl f = P.β€-thin _ _ cat .assoc f g h = P.β€-thin _ _ cat .Hom-set x y = is-propβis-set P.β€-thin {-# DISPLAY poset-to-category.cat P = posetβcategory P #-}
Our functor into is similarly easy to describe: Monotonicity of a map is functoriality when preservation of composites is automatic.
open Functor PosetsβͺStrict-cats : β {β ββ²} β Functor (Posets β ββ²) (Strict-cats β ββ²) PosetsβͺStrict-cats .Fβ P = posetβcategory P , Poset.has-is-set P PosetsβͺStrict-cats .Fβ f .Fβ = f .hom PosetsβͺStrict-cats .Fβ f .Fβ = f .preserves _ _ PosetsβͺStrict-cats .Fβ {y = y} f .F-id = Poset.β€-thin y _ _ PosetsβͺStrict-cats .Fβ {y = y} f .F-β g h = Poset.β€-thin y _ _ PosetsβͺStrict-cats .F-id = Functor-path (Ξ» _ β refl) Ξ» _ β refl PosetsβͺStrict-cats .F-β f g = Functor-path (Ξ» _ β refl) Ξ» _ β refl