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 _ _ _ _