module Order.Base where

Partially ordered setsπŸ”—

A poset is a set equipped with a relation x≀yx \le y, called a partial order, which is reflexive, transitive, and antisymmetric. Put another way, a poset is a univalent category which has at most one morphism between each pair of its objects: a thin category.

Posets are a simultaneous generalisation of many naturally occurring notions of β€œorder” in mathematics:

  • The β€œusual” ordering relations x≀yx \le y on familiar number systems like the natural numbers, the integers, the rationals, or the reals.

    When ordering the naturals, the integers, and the rationals, we can say more: they are linear orders. That is, in addition to the properties of ≀\le required to be a poset, we have, for any pair of elements xx and yy,

    (x≀y)∨(y≀x).(x \le y) \lor (y \le x)\text{.}

  • The divisibility order on the natural numbers is also a poset, as detailed in that page. More than just a poset, it’s actually a lattice: the meet of a pair of numbers is their greatest common divisor, and the join is their least common multiple.

    The divisibility ordering is also interesting as a counterexample: even though it is decidable, it fails to be a linear order: any pair of coprime numbers is unrelated by the divisibility order.

  • Moving away from numbers, partial orders are also intimately connected with the study of logic.

    To each theory T\mathbb{T} in a given fragment of propositional logic, we can build a set L(T)\mathcal{L}(\mathbb{T}) of sentences in the language of T\mathbb{T}; The entailment (or provability) relation Ο•βŠ’Οˆ\phi \vdash \psi is almost a partial order: we certainly have Ο•βŠ’Ο•\phi \vdash \phi, and the transitivity requirement is the β€œcut” rule,

    Ο•βŠ’ΟˆΟˆβŠ’ΞΈΟ•βŠ’ΞΈ. \frac {\phi \vdash \psi \quad \psi \vdash \theta} {\phi \vdash \theta\text{.}}

    However, this fails to be a poset, because inter-provable formulas Ο•βŠ’Οˆ\phi \vdash \psi and ΟˆβŠ’Ο•\psi \vdash \phi need not be syntactically equal. However, if we quotient the set L(T)\mathcal{L}(\mathbb{T}) by the inter-provability relation, then we do obtain a poset: the Lindenbaum-Tarski algebra of T\mathbb{T}.

    This poset will inherit order-theoretic structure from the logical structure of T\mathbb{T}: For example, if T\mathbb{T} is expressed in a fragment of logic which has conjunction, then L(T)\mathcal{L}(\mathbb{T}) will be a meet-semilattice; if it also has infinitary disjunction, then its Lindenbaum-Tarski algebra is a frame.

  • As mentioned in the opening paragraph, the notion of poset specialises that of univalent category.

    In particular, to every univalent category C\mathcal{C}, we can universally associate a poset: Its set of elements is the set truncation of C\mathcal{C}’s groupoid of objects, and the relation x≀yx \le y is the propositional truncation βˆ₯Hom(x,y)βˆ₯\| \mathbf{Hom}(x,y) \|.

    This process can actually be extended to any precategory: however, instead of merely truncating the space of objects, we must instead take its set-quotient by the relation x≀y∧y≀xx \le y \land y \le x.

With the motivating examples out of the way, we can finally move onto the formalised definition of poset, which is a straightforward translation.

record Poset o β„“ : Type (lsuc (o βŠ” β„“)) where
  no-eta-equality
  field
    Ob        : Type o
    _≀_       : Ob β†’ Ob β†’ Type β„“
    ≀-thin    : βˆ€ {x y} β†’ is-prop (x ≀ y)

We note, as usual, that each fibre x≀yx \le y of the order relation should be a proposition: this is precisely the formalisation of having at most one element. The reflexivity, transitivity, and antisymmetry properties are literal:

    ≀-refl    : βˆ€ {x}     β†’ x ≀ x
    ≀-trans   : βˆ€ {x y z} β†’ x ≀ y β†’ y ≀ z β†’ x ≀ z
    ≀-antisym : βˆ€ {x y}   β†’ x ≀ y β†’ y ≀ x β†’ x ≑ y

Note that the type of ≀-antisym ends in a path in Ob, which, a priori, might not be a proposition: we have not included the assumption that Ob is actually a set. Therefore, it might be the case that an identification between posets does not correspond to an identification of the underlying types and one of the relation. However, since the β€œsymmetric part” of ≀\le, the relation iff.

x∼y=(x≀y)∧(y≀x), x \sim y = (x \le y) \land (y \le x)\text{,}

is a reflexive mere relation which implies identity, the type of objects is automatically a set.

  abstract
    Ob-is-set : is-set Ob
    Ob-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)

Monotone mapsπŸ”—

Since we are considering posets to be categories satisfying a property, it follows that the category of posets should be a full subcategory of Cat\mathbf{Cat}; i.e., the maps Pβ†’QP \to Q should be precisely the functors Pβ†’QP \to Q. However, since there is at most one inhabitant of each f(x)≀f(y)f(x) \le f(y), we are free to drop the functoriality assumptions, and consider instead the monotone maps:

record
  Monotone {o o' β„“ β„“'} (P : Poset o β„“) (Q : Poset o' β„“')
    : Type (o βŠ” o' βŠ” β„“ βŠ” β„“') where
  no-eta-equality
  field
    hom    : P.Ob β†’ Q.Ob
    pres-≀ : βˆ€ {x y} β†’ x P.≀ y β†’ hom x Q.≀ hom y

A monotone map between posets is a map between their underlying sets which preserves the order relation. This is the most natural choice: for example, the monotone functions (N,≀)β†’P(\mathbb{N}, \le) \to P are precisely nondecreasing sequences of elements in PP.

It’s immediate to see that the identity function is monotone, and that monotone maps are closed under composition. Since identity of monotone maps is given by identity of the underlying functions, there is a set of monotone maps Pβ†’QP \to Q, and the laws of a category are trivial.

idβ‚˜ : Monotone P P
idβ‚˜ .hom    x   = x
idβ‚˜ .pres-≀ x≀y = x≀y

_βˆ˜β‚˜_ : Monotone Q R β†’ Monotone P Q β†’ Monotone P R
(f βˆ˜β‚˜ g) .hom    x   = f # (g # x)
(f βˆ˜β‚˜ g) .pres-≀ x≀y = f .pres-≀ (g .pres-≀ x≀y)

Posets : βˆ€ (o β„“ : Level) β†’ Precategory (lsuc o βŠ” lsuc β„“) (o βŠ” β„“)
Posets o β„“ .Precategory.Ob      = Poset o β„“
Posets o β„“ .Precategory.Hom     = Monotone
Posets o β„“ .Precategory.Hom-set = hlevel!

Posets o β„“ .Precategory.id  = idβ‚˜
Posets o β„“ .Precategory._∘_ = _βˆ˜β‚˜_

Posets o β„“ .Precategory.idr f       = trivial!
Posets o β„“ .Precategory.idl f       = trivial!
Posets o β„“ .Precategory.assoc f g h = trivial!

Simple constructionsπŸ”—

The simplest thing we can do to a poset is to forget the order. This evidently extends to a faithful functor Pos→Sets\mathbf{Pos} \to \mathbf{Sets}.

Forget-poset : βˆ€ {o β„“} β†’ Functor (Posets o β„“) (Sets o)
∣ Forget-poset .Functor.Fβ‚€ P ∣    = ⌞ P ⌟
Forget-poset .Functor.Fβ‚€ P .is-tr = hlevel!

Forget-poset .Functor.F₁ = hom

Forget-poset .Functor.F-id    = refl
Forget-poset .Functor.F-∘ _ _ = refl

Slightly less trivial, we can extend the opposite category construction to posets as well, by transposing the order relation and making sure to flip the direction of transitivity:

_^opp : βˆ€ {β„“ β„“'} β†’ Poset β„“ β„“' β†’ Poset β„“ β„“'
(P ^opp) .Poset.Ob      = Poset.Ob P
(P ^opp) .Poset._≀_ x y = Poset._≀_ P y x

(P ^opp) .Poset.≀-thin = Poset.≀-thin P
(P ^opp) .Poset.≀-refl = Poset.≀-refl P
(P ^opp) .Poset.≀-trans   xβ‰₯y yβ‰₯z = Poset.≀-trans P yβ‰₯z xβ‰₯y
(P ^opp) .Poset.≀-antisym xβ‰₯y yβ‰₯x = Poset.≀-antisym P yβ‰₯x xβ‰₯y

We can construct the trivial posets with one and zero (object(s), ordering(s)) respectively


πŸ™α΅– : βˆ€ {o β„“} β†’ Poset o β„“
πŸ™α΅– .Poset.Ob = Lift _ ⊀
πŸ™α΅– .Poset._≀_ _ _ = Lift _ ⊀
πŸ™α΅– .Poset.≀-thin = hlevel!
πŸ™α΅– .Poset.≀-refl = lift tt
πŸ™α΅– .Poset.≀-trans = Ξ» _ _ β†’ lift tt
πŸ™α΅– .Poset.≀-antisym = Ξ» _ _ β†’ refl

πŸ˜α΅– : βˆ€ {o β„“} β†’ Poset o β„“
πŸ˜α΅– .Poset.Ob = Lift _ βŠ₯
πŸ˜α΅– .Poset._≀_ _ _ = Lift _ βŠ₯
πŸ˜α΅– .Poset.≀-thin ()
πŸ˜α΅– .Poset.≀-refl {()}
πŸ˜α΅– .Poset.≀-trans ()
πŸ˜α΅– .Poset.≀-antisym ()