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 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 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 required to be a poset, we have, for any pair of elements and

• 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 in a given fragment of propositional logic, we can build a set of sentences in the language of The entailment (or provability) relation is almost a partial order: we certainly have and the transitivity requirement is the βcutβ rule,

However, this fails to be a poset, because inter-provable formulas and need not be syntactically equal. However, if we quotient the set by the inter-provability relation, then we do obtain a poset: the Lindenbaum-Tarski algebra of

This poset will inherit order-theoretic structure from the logical structure of For example, if is expressed in a fragment of logic which has conjunction, then 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 we can universally associate a poset: Its set of elements is the set truncation of groupoid of objects, and the relation is the propositional truncation

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

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 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 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 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)

  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 2))
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 1))
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 i.e., the maps should be precisely the functors However, since there is at most one inhabitant of each 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 are precisely nondecreasing sequences of elements in

open Monotone public

private variable
o β o' β' o'' β'' : Level
P Q R : Poset o β

unquoteDecl H-Level-Monotone = declare-record-hlevel 2 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} 1
Ξ» 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 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 2

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

PosetsβͺSets : β {o β} β Functor (Posets o β) (Sets o)
PosetsβͺSets .Functor.Fβ P .β£_β£    = β P β
PosetsβͺSets .Functor.Fβ P .is-tr = hlevel 2
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 1
πα΅ .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 ()