module Order.Instances.Pointwise where

The pointwise orderingπŸ”—

The product of a family of partially ordered sets is a poset, for any index 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 : βˆ€ {β„“ ℓₐ β„“α΅£} (I : Type β„“) (P : I β†’ Poset ℓₐ β„“α΅£)
  β†’ Poset (β„“ βŠ” ℓₐ) (β„“ βŠ” β„“α΅£)
Pointwise I P = po where
  open module PrP {i : I} = Pr (P i)

  po : Poset _ _
  po .Poset.Ob = (i : I) β†’ ⌞ P i ⌟
  po .Poset._≀_ f g = βˆ€ x β†’ f x ≀ g x
  po .Poset.≀-thin = hlevel 1
  po .Poset.≀-refl x = ≀-refl
  po .Poset.≀-trans f≀g g≀h x = ≀-trans (f≀g x) (g≀h x)
  po .Poset.≀-antisym f≀g g≀f = funext Ξ» x β†’ ≀-antisym (f≀g x) (g≀f x)

  : βˆ€ {β„“ ℓₐ ℓₐ' β„“α΅£ β„“α΅£'} {I : Type β„“} {P : I β†’ Poset ℓₐ β„“α΅£} {R : Poset ℓₐ' β„“α΅£'}
  β†’ (βˆ€ i β†’ Monotone R (P i))
  β†’ Monotone R (Pointwise I P)
tupleα΅– f .hom x i = f i # x
tupleα΅– f .pres-≀ x≀y i = f i .pres-≀ x≀y

  : βˆ€ {β„“ ℓₐ β„“α΅£} {I : Type β„“} {P : I β†’ Poset ℓₐ β„“α΅£} (i : I)
  β†’ Monotone (Pointwise I P) (P i)
prjα΅– i .hom f      = f i
prjα΅– i .pres-≀ f≀g = f≀g i

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:

  : βˆ€ {β„“β‚’ β„“α΅£ β„“β‚’' β„“α΅£'}
  β†’ (P : Poset β„“β‚’ β„“α΅£) (Q : Poset β„“β‚’' β„“α΅£')
  β†’ Poset (β„“β‚’ βŠ” β„“α΅£ βŠ” β„“β‚’' βŠ” β„“α΅£') (β„“β‚’ βŠ” β„“α΅£')
Poset[_,_] P Q = po module Poset[_,_] where
  open Pr Q

  po : Poset _ _
  po .Poset.Ob      = Monotone P Q
  po .Poset._≀_ f g = βˆ€ (x : ⌞ P ⌟) β†’ f # x ≀ g # x

  po .Poset.≀-thin   = hlevel 1
  po .Poset.≀-refl _ = ≀-refl

  po .Poset.≀-trans   f≀g g≀h x = ≀-trans (f≀g x) (g≀h x)
  po .Poset.≀-antisym f≀g g≀f   = ext Ξ» x β†’ ≀-antisym (f≀g x) (g≀f x)

Using Pointwise we can show that has all indexed products:

  : βˆ€ {o β„“ β„“'}
  β†’ has-indexed-products (Posets (o βŠ” β„“') (β„“ βŠ” β„“')) β„“'
Posets-has-indexed-products F = mk where
  mk : Indexed-product (Posets _ _) _
  mk .Ξ F = Pointwise _ F
  mk .Ο€  = prjα΅–
  mk .has-is-ip .tuple   = tupleα΅–
  mk .has-is-ip .commute = trivial!
  mk .has-is-ip .unique f g = ext Ξ» y i β†’ g i #β‚š y

Binary products are a special case of indexed productsπŸ”—

×≑Pointwise-bool : βˆ€ {o β„“} (P Q : Poset o β„“) β†’ P Γ—α΅– Q ≑ Pointwise Bool (if_then P else Q)
×≑Pointwise-bool P Q = Poset-path Ξ» where
  .to   β†’ tupleα΅– (Bool-elim _ fstα΅– sndα΅–)
  .from β†’ pairα΅– (prjα΅– true) (prjα΅– false)
  .inverses .invl β†’ ext Ξ» where
    x true β†’ refl
    x false β†’ refl
  .inverses .invr β†’ ext Ξ» x y β†’ refl , refl