open import Cat.Instances.StrictCat
open import Cat.Instances.Functor
open import Cat.Prelude

open import Order.Base

import Order.Reasoning

open Precategory

module Order.Cat where


# Posets as categoriesπ

We have already remarked a poset is a special kind of category: a thin category, i.e.Β one that has propositional sets.

is-thin : β {β β'} β Precategory β β' β Type (β β β')
is-thin C = β x y β is-prop (C .Hom x y)


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 : β {β β'} β Poset β β' β Precategory β β'
posetβcategory P = cat module poset-to-category where
module P = Poset P

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 #-}

posetβthin : β {β β'} (P : Poset β β') β is-thin (posetβcategory P)
posetβthin P _ _ = P.β€-thin where module P = Poset 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.Ob-is-set P

PosetsβͺStrict-cats .Fβ f .Fβ = f .hom
PosetsβͺStrict-cats .Fβ f .Fβ = f .pres-β€
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


More generally, to give a functor into a thin category, it suffices to give the action on objects and morphisms: the laws hold automatically.

module
_ {oc od βc βd} {C : Precategory oc βc} {D : Precategory od βd}
(D-thin : is-thin D)
where

thin-functor
: (f : C .Ob β D .Ob)
β (fβ : β {x y} β C .Hom x y β D .Hom (f x) (f y))
β Functor C D
thin-functor f fβ .Fβ = f
thin-functor f fβ .Fβ = fβ
thin-functor f fβ .F-id = D-thin _ _ _ _
thin-functor f fβ .F-β _ _ = D-thin _ _ _ _