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, which additionally satisfies the property that there is at most one morphism inhabiting each Hom\mathbf{Hom}-set.

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

  opaque
    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

Poset-on-pathp
  : βˆ€ {o β„“} {A B : Type o}
  β†’ {A-poset : Poset-on β„“ A} {B-poset : Poset-on β„“ B}
  β†’ (p : A ≑ B)
  β†’ PathP (Ξ» i β†’ p i β†’ p i β†’ Type β„“) (Poset-on._≀_ A-poset) (Poset-on._≀_ B-poset)
  β†’ PathP (Ξ» i β†’ Poset-on β„“ (p i)) A-poset B-poset
Poset-on-pathp p q i .Poset-on._≀_ = q i
Poset-on-pathp {A-poset = A-poset} {B-poset = B-poset} p q i .Poset-on.has-is-poset =
  is-prop→pathp (λ i → is-partial-order-is-prop (q i))
    (Poset-on.has-is-poset A-poset)
    (Poset-on.has-is-poset B-poset) i

Poset-on-path
  : βˆ€ {o β„“} {A : Type o}
  β†’ {P Q : Poset-on β„“ A}
  β†’ (βˆ€ x y β†’ Poset-on._≀_ P x y ≑ Poset-on._≀_ Q x y)
  β†’ P ≑ Q
Poset-on-path p = Poset-on-pathp refl (funext Ξ» x β†’ funext Ξ» y β†’ p x y)

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!

is-monotone
  : βˆ€ {o o' β„“ β„“'} {A : Type o} {B : Type o'}
  β†’ (f : A β†’ B) β†’ Poset-on β„“ A β†’ Poset-on β„“' B β†’ Type _
is-monotone f P Q = βˆ€ x y β†’ x P.≀ y β†’ f x Q.≀ f y
  where
    module P = Poset-on P
    module Q = Poset-on Q

is-monotone-is-prop
  : βˆ€ {o o' β„“ β„“'} {A : Type o} {B : Type o'}
  β†’ (f : A β†’ B) (P : Poset-on β„“ A) (Q : Poset-on β„“' B)
  β†’ is-prop (is-monotone f P Q)
is-monotone-is-prop f P Q =
  Ξ -is-hlevelΒ³ 1 Ξ» _ _ _ β†’ Poset-on.≀-thin Q

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

Poset-structure β„“ β„“β€² .is-hom f P Q .is-tr =
  is-monotone-is-prop f P 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} Ξ± Ξ² =
  Poset-on-path Ξ» x y β†’ ua (prop-ext s.≀-thin t.≀-thin (Ξ± x y) (Ξ² x y))
  where
    module s = Poset-on s
    module t = Poset-on t

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

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

Posets-is-category : βˆ€ {o β„“} β†’ is-category (Posets o β„“)
Posets-is-category = Structured-objects-is-category (Poset-structure _ _)

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β†©οΈŽ