open import 1Lab.Reflection

open import Cat.Prelude

import Cat.Reasoning

module Order.Base where

Partially ordered sets🔗

A poset is a set equipped with a relation $x\le y\text{,}$ 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\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 $x$ and $y\text{,}$

  $$(x\le y)\vee (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 $\mathbb{T}$ in a given fragment of propositional logic, we can build a set $\mathcal{L}(\mathbb{T})$ of sentences in the language of $\mathbb{T}\text{;}$ The entailment (or provability) relation $\phi ⊢\psi$ is almost a partial order: we certainly have $\phi ⊢\phi \text{,}$ and the transitivity requirement is the “cut” rule,

  $$\frac{\phi ⊢\psi \psi ⊢\theta }{\phi ⊢\theta \text{.}}$$

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

  This poset will inherit order-theoretic structure from the logical structure of $\mathbb{T}\text{:}$ For example, if $\mathbb{T}$ is expressed in a fragment of logic which has conjunction, then $\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 $\mathcal{C}\text{,}$ we can universally associate a poset: Its set of elements is the set truncation of $\mathcal{C}\text{’s}$ groupoid of objects, and the relation $x\le y$ is the propositional truncation $\Vert \mathbf{Hom}(x,y)\Vert \text{.}$

  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\le y\wedge y\le x\text{.}$

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\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 \text{,}$ the relation iff.

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 
        {r = λ _ → ≤-refl , ≤-refl}
        (set-identity-system
          (λ a b → ×-is-hlevel  ≤-thin ≤-thin)
          (λ {a} {b} (p , q) → ≤-antisym {a} {b} p q))
        (λ a b → ×-is-hlevel  ≤-thin ≤-thin)

  abstract
    ≤-refl' : ∀ {x y} → x ≡ y → x ≤ y
    ≤-refl' {x = x} p = subst (x ≤_) p ≤-refl

instance
  Underlying-Poset : ∀ {o ℓ} → Underlying (Poset o ℓ)
  Underlying-Poset .Underlying.ℓ-underlying = _
  Underlying-Poset .Underlying.⌞_⌟ = Poset.Ob

  open hlevel-projection

  Poset-ob-hlevel-proj : hlevel-projection (quote Poset.Ob)
  Poset-ob-hlevel-proj .has-level   = quote Poset.Ob-is-set
  Poset-ob-hlevel-proj .get-level _ = pure (lit (nat ))
  Poset-ob-hlevel-proj .get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
  Poset-ob-hlevel-proj .get-argument _                     = typeError []

  Poset-≤-hlevel-proj : hlevel-projection (quote Poset._≤_)
  Poset-≤-hlevel-proj .has-level   = quote Poset.≤-thin
  Poset-≤-hlevel-proj .get-level _ = pure (lit (nat ))
  Poset-≤-hlevel-proj .get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
  Poset-≤-hlevel-proj .get-argument _                     = typeError []

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 $\mathbf{Cat}\text{;}$ i.e., the maps $P\to Q$ should be precisely the functors $P\to Q\text{.}$ However, since there is at most one inhabitant of each $f(x)\le f(y)\text{,}$ 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

  private
    module P = Poset P
    module Q = Poset Q

  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 $(\mathbb{N},\le )\to P$ are precisely nondecreasing sequences of elements in $P\text{.}$

open Monotone public

private variable
  o ℓ o' ℓ' o'' ℓ'' : Level
  P Q R : Poset o ℓ

unquoteDecl H-Level-Monotone = declare-record-hlevel  H-Level-Monotone (quote Monotone)

instance
  Funlike-Monotone : Funlike (Monotone P Q) ⌞ P ⌟ λ _ → ⌞ Q ⌟
  Funlike-Monotone = record { _#_ = hom }

  Membership-Monotone : ⦃ _ : Underlying ⌞ Q ⌟ ⦄ → Membership ⌞ P ⌟ (Monotone P Q) _
  Membership-Monotone = record { _∈_ = λ x S → ⌞ S # x ⌟ }

Monotone-pathp
  : ∀ {o ℓ o' ℓ'} {P : I → Poset o ℓ} {Q : I → Poset o' ℓ'}
  → {f : Monotone (P i0) (Q i0)} {g : Monotone (P i1) (Q i1)}
  → PathP (λ i → ⌞ P i ⌟ → ⌞ Q i ⌟) (apply f) (apply g)
  → PathP (λ i → Monotone (P i) (Q i)) f g
Monotone-pathp q i .hom a = q i a
Monotone-pathp {P = P} {Q} {f} {g} q i .Monotone.pres-≤ {x} {y} α =
  is-prop→pathp
    (λ i → Π-is-hlevel³ {A = ⌞ P i ⌟} {B = λ _ → ⌞ P i ⌟} {C = λ x y → P i .Poset._≤_ x y} 
      λ x y _ → Q i .Poset.≤-thin {q i x} {q i y})
    (λ _ _ α → f .Monotone.pres-≤ α)
    (λ _ _ α → g .Monotone.pres-≤ α) i x y α

instance
  Extensional-Monotone
    : ∀ {o ℓ o' ℓ' ℓr} {P : Poset o ℓ} {Q : Poset o' ℓ'}
    → ⦃ sa : Extensional (⌞ P ⌟ → ⌞ Q ⌟) ℓr ⦄
    → Extensional (Monotone P Q) ℓr
  Extensional-Monotone {Q = Q} ⦃ sa ⦄ =
    injection→extensional! Monotone-pathp sa

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\to Q\text{,}$ 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!

module Posets {o ℓ} = Cat.Reasoning (Posets o ℓ)

Simple constructions🔗

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

Posets↪Sets : ∀ {o ℓ} → Functor (Posets o ℓ) (Sets o)
Posets↪Sets .Functor.F₀ P .∣_∣    = ⌞ P ⌟
Posets↪Sets .Functor.F₀ P .is-tr = hlevel 
Posets↪Sets .Functor.F₁ = hom
Posets↪Sets .Functor.F-id    = refl
Posets↪Sets .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 ()