open import Cat.Prelude

open import Order.Instances.Props
open import Order.Displayed
open import Order.Base

import Order.Reasoning as Pr

module Order.Instances.Pointwise where

The pointwise orderingπŸ”—

If (B,≀)(B, \le) is a partially ordered set, then so is Aβ†’BA \to B, for any type AA which we might choose! There might be other ways of making Aβ†’BA \to B into a poset, of course, but the canonical way we’re talking about here is the pointwise ordering on Aβ†’BA \to B, where f≀gf \le g iff f(x)≀g(x)f(x) \le g(x) for all xx.

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 A→ΩA \to \Omega.

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 P→QP \to Q 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