open import Cat.Displayed.Univalence.Thin
open import Cat.Instances.StrictCat
open import Cat.Instances.Functor
open import Cat.Prelude

open import Order.Base

import Order.Reasoning as Poset

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 Catstrict\mathfrak{Cat}_\mathrm{strict} 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