open import Cat.Displayed.Univalence.Thin
open import Cat.Prelude

module Order.Base where

Partially ordered setsπŸ”—

A poset (short for partially ordered set) is a set equipped with a relation x≀yx \le y which is reflexive, transitive and antisymmetric. Put another way, a poset is a univalent category having at most one morphism between each pair of elements.

For convenience reasons, we prefer not to work with the category generated by a poset: the category associated with a poset reifies a lot of redundant information, which is necessary when working with Hom\mathbf{Hom}-sets, but not with Hom\mathbf{Hom}-props. Working with the generated category is analogous to only ever working with locally discrete bicategories: you could, but then you’d be hauling around a bunch of redundant information.

Another reason to define posets as their own concept, rather than as a special case of categories, is using our pre-existing infrastructure for constructing very convenient categories of sets-with-structure; In this case, sets with β€œpo” structure!

We start by defining the predicate is-partial-order on a relation x≀yx \le y. That it turns out to be a predicate is actually slightly nontrivial: The first four components are manifestly propositional, but the last component β€” the witness of antisymmetry β€” could really gunk things up, since it has the potential to assign loops! But, given any antisymmetric relation x≀yx \le y, the family

(x,y)↦(x≀y)∧(y≀x) (x, y) \mapsto (x \le y) \land (y \le x)

is an identity system1 on AA; and, being a product of propositions, it’s also a proposition, so AA is automatically a set.

record is-partial-order {β„“ β„“β€²} {A : Type β„“}
          (_≀_ : A β†’ A β†’ Type β„“β€²) : Type (β„“ βŠ” β„“β€²) where
  no-eta-equality
  field
    ≀-thin    : βˆ€ {x y} β†’ is-prop (x ≀ y)
    ≀-refl    : βˆ€ {x} β†’ x ≀ x
    ≀-trans   : βˆ€ {x y z} β†’ x ≀ y β†’ y ≀ z β†’ x ≀ z
    ≀-antisym : βˆ€ {x y} β†’ x ≀ y β†’ y ≀ x β†’ x ≑ y

  has-is-set : is-set A
  has-is-set =
    identity-system→hlevel 1
      {r = Ξ» _ β†’ ≀-refl , ≀-refl}
      (set-identity-system
        (Ξ» a b β†’ Γ—-is-hlevel 1 ≀-thin ≀-thin)
        (Ξ» {a} {b} (p , q) β†’ ≀-antisym {a} {b} p q))
      (Ξ» a b β†’ Γ—-is-hlevel 1 ≀-thin ≀-thin)

private unquoteDecl eqv = declare-record-iso eqv (quote is-partial-order)

is-partial-order-is-prop
  : βˆ€ {β„“ β„“β€²} {A : Type β„“} (R : A β†’ A β†’ Type β„“β€²) β†’ is-prop (is-partial-order R)
is-partial-order-is-prop {A = A} R x y = go x x y where
  go : is-partial-order R β†’ is-prop (is-partial-order R)
  go x = Iso→is-hlevel 1 eqv (hlevel 1) where instance
    h-level-r : βˆ€ {x y} {n} β†’ H-Level (R x y) (suc n)
    h-level-r = prop-instance (x .is-partial-order.≀-thin)

    h-level-a : H-Level A 2
    h-level-a = basic-instance 2 (is-partial-order.has-is-set x)

A po structure on a set β€” okay, that joke is getting old β€” is given by tupling together the relation x≀yx \le y together with a proof that it is a partial order relation. Identity of poset structures is thus determined by identity of the relations, since being a partial order is a proposition.

record Poset-on {β„“} β„“β€² (A : Type β„“) : Type (β„“ βŠ” lsuc β„“β€²) where
  no-eta-equality
  field
    _≀_          : A β†’ A β†’ Type β„“β€²
    has-is-poset : is-partial-order _≀_
  open is-partial-order has-is-poset public

We set up the category of posets using our machinery for displaying univalent categories over the category of sets. A map between posets is called a monotone map: it’s the decategorification of a functor. We don’t need preservation of identities or preservation of composites, since our β€œhoms” are propositions!

Poset-structure : βˆ€ β„“ β„“β€² β†’ Thin-structure {β„“ = β„“} (β„“ βŠ” β„“β€²) (Poset-on β„“β€²)
∣ Poset-structure β„“ β„“β€² .is-hom f P Q ∣ =
  βˆ€ x y β†’ Poset-on._≀_ P x y β†’ Poset-on._≀_ Q (f x) (f y)

Poset-structure β„“ β„“β€² .is-hom f P Q .is-tr =
  Ξ -is-hlevelΒ³ 1 Ξ» _ _ _ β†’ Poset-on.≀-thin Q

Poset-structure β„“ β„“β€² .id-is-hom x y Ξ± = Ξ±
Poset-structure β„“ β„“β€² .∘-is-hom f g Ξ± Ξ² x y Ξ³ = Ξ± (g x) (g y) (Ξ² x y Ξ³)

The last thing we have to prove is β€œuniqueness of identity maps”: If we have the identity being a monotone map (a,t)β†’(a,s)(a, t) \to (a, s) and (a,s)β†’(a,t)(a, s) \to (a, t) β€” that is, we have (x≀sy)↔(x≀ty)(x \le_s y) \leftrightarrow (x \le_t y) β€” then, by propositional extensionality, we have ≀s=≀t\le_s = \le_t. Then, since equality of poset structures is controlled by equality of the relations, we have s=ts = t!

Poset-structure β„“ β„“β€² .id-hom-unique {s = s} {t = t} Ξ± Ξ² = q where
  module s = Poset-on s
  module t = Poset-on t
  open is-iso

  p : s._≀_ ≑ t._≀_
  p i x y = ua (prop-ext s.≀-thin t.≀-thin (Ξ± x y) (Ξ² x y)) i

  q : s ≑ t
  q i .Poset-on._≀_ = p i
  q i .Poset-on.has-is-poset = is-prop→pathp
    (Ξ» i β†’ is-partial-order-is-prop (p i))
    s.has-is-poset t.has-is-poset i

Posets : βˆ€ β„“ β„“β€² β†’ Precategory (lsuc (β„“ βŠ” β„“β€²)) (β„“ βŠ” β„“β€²)
Posets β„“ β„“β€² = Structured-objects (Poset-structure β„“ β„“β€²)

module Posets {β„“ β„“β€²} = Precategory (Posets β„“ β„“β€²)
Poset : (β„“ β„“β€² : Level) β†’ Type (lsuc (β„“ βŠ” β„“β€²))
Poset β„“ β„“β€² = Precategory.Ob (Posets β„“ β„“β€²)

record make-poset {β„“} β„“β€² (A : Type β„“) : Type (β„“ βŠ” lsuc β„“β€²) where
  no-eta-equality

  field
    rel     : A β†’ A β†’ Type β„“β€²
    id      : βˆ€ {x} β†’ rel x x
    thin    : βˆ€ {x y} β†’ is-prop (rel x y)
    trans   : βˆ€ {x y z} β†’ rel x y β†’ rel y z β†’ rel x z
    antisym : βˆ€ {x y} β†’ rel x y β†’ rel y x β†’ x ≑ y

  to-poset-on : Poset-on β„“β€² A
  to-poset-on .Poset-on._≀_ = rel
  to-poset-on .Poset-on.has-is-poset .is-partial-order.≀-thin = thin
  to-poset-on .Poset-on.has-is-poset .is-partial-order.≀-refl = id
  to-poset-on .Poset-on.has-is-poset .is-partial-order.≀-trans = trans
  to-poset-on .Poset-on.has-is-poset .is-partial-order.≀-antisym = antisym

to-poset : βˆ€ {β„“ β„“β€²} (A : Type β„“) β†’ make-poset β„“β€² A β†’ Poset β„“ β„“β€²
∣ to-poset A mk .fst ∣ = A
to-poset A mk .fst .is-tr = Poset-on.has-is-set (make-poset.to-poset-on mk)
to-poset A mk .snd = make-poset.to-poset-on mk

The relationship between posets and (strict) categories is outlined in the module Order.Cat. Very similarly to categories, posets have a duality involution. In fact, under the correspondence between posets and thin categories, these are the same construction.

_^opp : βˆ€ {β„“ β„“β€²} β†’ Poset β„“ β„“β€² β†’ Poset β„“ β„“β€²
P ^opp = to-poset ⌞ P ⌟ λ where
    .make-poset.rel x y         β†’ y ≀ x
    .make-poset.thin            β†’ ≀-thin
    .make-poset.id              β†’ ≀-refl
    .make-poset.trans f<g g<h   β†’ ≀-trans g<h f<g
    .make-poset.antisym f<g g<f β†’ ≀-antisym g<f f<g
  where open Poset-on (P .snd)

  1. Together with the unique evidence that this is a reflexive relationβ†©οΈŽ