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, which additionally satisfies the property that there is at most one morphism inhabiting each -set.
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 opaque 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
Poset-on-pathp : β {o β} {A B : Type o} β {A-poset : Poset-on β A} {B-poset : Poset-on β B} β (p : A β‘ B) β PathP (Ξ» i β p i β p i β Type β) (Poset-on._β€_ A-poset) (Poset-on._β€_ B-poset) β PathP (Ξ» i β Poset-on β (p i)) A-poset B-poset Poset-on-pathp p q i .Poset-on._β€_ = q i Poset-on-pathp {A-poset = A-poset} {B-poset = B-poset} p q i .Poset-on.has-is-poset = is-propβpathp (Ξ» i β is-partial-order-is-prop (q i)) (Poset-on.has-is-poset A-poset) (Poset-on.has-is-poset B-poset) i Poset-on-path : β {o β} {A : Type o} β {P Q : Poset-on β A} β (β x y β Poset-on._β€_ P x y β‘ Poset-on._β€_ Q x y) β P β‘ Q Poset-on-path p = Poset-on-pathp refl (funext Ξ» x β funext Ξ» y β p x y)
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!
is-monotone : β {o o' β β'} {A : Type o} {B : Type o'} β (f : A β B) β Poset-on β A β Poset-on β' B β Type _ is-monotone f P Q = β x y β x P.β€ y β f x Q.β€ f y where module P = Poset-on P module Q = Poset-on Q is-monotone-is-prop : β {o o' β β'} {A : Type o} {B : Type o'} β (f : A β B) (P : Poset-on β A) (Q : Poset-on β' B) β is-prop (is-monotone f P Q) is-monotone-is-prop f P Q = Ξ -is-hlevelΒ³ 1 Ξ» _ _ _ β Poset-on.β€-thin Q Poset-structure : β β ββ² β Thin-structure {β = β} (β β ββ²) (Poset-on ββ²) β£ Poset-structure β ββ² .is-hom f P Q β£ = is-monotone f P Q Poset-structure β ββ² .is-hom f P Q .is-tr = is-monotone-is-prop f P 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} Ξ± Ξ² = Poset-on-path Ξ» x y β ua (prop-ext s.β€-thin t.β€-thin (Ξ± x y) (Ξ² x y)) where module s = Poset-on s module t = Poset-on t
Posets : β β ββ² β Precategory (lsuc (β β ββ²)) (β β ββ²) Posets β ββ² = Structured-objects (Poset-structure β ββ²) module Posets {β ββ²} = Precategory (Posets β ββ²) Poset : (β ββ² : Level) β Type (lsuc (β β ββ²)) Poset β ββ² = Precategory.Ob (Posets β ββ²) Posets-is-category : β {o β} β is-category (Posets o β) Posets-is-category = Structured-objects-is-category (Poset-structure _ _) 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β©οΈ