open import Cat.Displayed.Univalence.Thin open import Cat.Prelude module Order.Base where

# Partially ordered setsπ

A **poset** (short for **p**artially
**o**rdered 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 system^{1} 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)

Together with the unique evidence that this is a reflexive relationβ©οΈ