module Order.Base where
Partially ordered setsπ
A poset (short for partially ordered set) is a set equipped with a relation 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 -sets, but not with -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 . 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 , the family
is an identity system1 on ; and, being a product of propositions, itβs also a proposition, so 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)
private unquoteDecl eqv = declare-record-iso eqv (quote is-partial-order) is-partial-order-is-prop : β {β ββ²} {A : Type β} (R : A β A β Type ββ²) β is-prop (is-partial-order R) is-partial-order-is-prop {A = A} R x y = go x x y where go : is-partial-order R β is-prop (is-partial-order R) go x = Isoβis-hlevel 1 eqv (hlevel 1) where instance h-level-r : β {x y} {n} β H-Level (R x y) (suc n) h-level-r = prop-instance (x .is-partial-order.β€-thin) h-level-a : H-Level A 2 h-level-a = basic-instance 2 (is-partial-order.has-is-set x)
A po structure on a set β okay, that joke is getting old β is given by tupling together the relation 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 and β that is, we have β then, by propositional extensionality, we have . Then, since equality of poset structures is controlled by equality of the relations, we have !
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
Posets : β β ββ² β Precategory (lsuc (β β ββ²)) (β β ββ²) Posets β ββ² = Structured-objects (Poset-structure β ββ²) module Posets {β ββ²} = Precategory (Posets β ββ²) Poset : (β ββ² : Level) β Type (lsuc (β β ββ²)) Poset β ββ² = Precategory.Ob (Posets β ββ²) record make-poset {β} ββ² (A : Type β) : Type (β β lsuc ββ²) where no-eta-equality field rel : A β A β Type ββ² id : β {x} β rel x x thin : β {x y} β is-prop (rel x y) trans : β {x y z} β rel x y β rel y z β rel x z antisym : β {x y} β rel x y β rel y x β x β‘ y to-poset-on : Poset-on ββ² A to-poset-on .Poset-on._β€_ = rel to-poset-on .Poset-on.has-is-poset .is-partial-order.β€-thin = thin to-poset-on .Poset-on.has-is-poset .is-partial-order.β€-refl = id to-poset-on .Poset-on.has-is-poset .is-partial-order.β€-trans = trans to-poset-on .Poset-on.has-is-poset .is-partial-order.β€-antisym = antisym to-poset : β {β ββ²} (A : Type β) β make-poset ββ² A β Poset β ββ² β£ to-poset A mk .fst β£ = A to-poset A mk .fst .is-tr = Poset-on.has-is-set (make-poset.to-poset-on mk) to-poset A mk .snd = make-poset.to-poset-on mk
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β©οΈ