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 \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 ${\mathbf{Hom}}$-sets, but not with ${\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 \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 \le y$, the family

$(x, y) \mapsto (x \le y) \land (y \le x)$

is an identity system1 on $A$; and, being a product of propositions, it’s also a proposition, so $A$ 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)


A po structure on a set — okay, that joke is getting old — is given by tupling together the relation $x \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) \to (a, s)$ and $(a, s) \to (a, t)$ — that is, we have $(x \le_s y) \leftrightarrow (x \le_t y)$ — then, by propositional extensionality, we have $\le_s = \le_t$. Then, since equality of poset structures is controlled by equality of the relations, we have $s = 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


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↩︎