module Order.Instances.Pointwise where
The pointwise orderingπ
If is a partially ordered set, then so is , for any type which we might choose! There might be other ways of making into a poset, of course, but the canonical way weβre talking about here is the pointwise ordering on , where iff for all .
Pointwise : β {β ββ βα΅£} β Type β β Poset ββ βα΅£ β Poset (β β ββ) (β β βα΅£) Pointwise A B = to-poset (A β β B β) mk-pwise where open Pr B mk-pwise : make-poset _ _ mk-pwise .make-poset.rel f g = β x β f x β€ g x mk-pwise .make-poset.thin = hlevel 1 mk-pwise .make-poset.id x = β€-refl mk-pwise .make-poset.trans f<g g<h x = β€-trans (f<g x) (g<h x) mk-pwise .make-poset.antisym f<g g<f = funext Ξ» x β β€-antisym (f<g x) (g<f x)
A very important particular case of the pointwise ordering is the poset of subsets of a fixed type, which has underlying set .
Subsets : β {β} β Type β β Poset β β Subsets A = Pointwise A Props
Another important case: when your domain is not an arbitrary type but another poset, you might want to consider the full subposet of consisting of the monotone maps:
Monotone : β {ββ βα΅£ βββ² βα΅£β²} β Poset ββ βα΅£ β Poset βββ² βα΅£β² β Poset (ββ β βα΅£ β βββ² β βα΅£β²) (ββ β βα΅£β²) Monotone P Q = Full-subposet (Pointwise β P β Q) Ξ» f β el! (β x y β x P.β€ y β f x Q.β€ f y) where module P = Pr P module Q = Pr Q