open import 1Lab.Reflection.Marker

open import Cat.Diagram.Product.Indexed
open import Cat.Morphism
open import Cat.Prelude

open import Data.Power
open import Data.Bool

open import Order.Instances.Product
open import Order.Semilattice.Join
open import Order.Semilattice.Meet
open import Order.Instances.Props
open import Order.Diagram.Bottom
open import Order.Diagram.Join
open import Order.Diagram.Meet
open import Order.Diagram.Glb
open import Order.Diagram.Lub
open import Order.Diagram.Top
open import Order.Univalent
open import Order.Base

import Order.Reasoning as Pr

open is-indexed-product
open Indexed-product
open Inverses

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)

tupleα΅–
  : βˆ€ {β„“ ℓₐ ℓₐ' β„“α΅£ β„“α΅£'} {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

prjα΅–
  : βˆ€ {β„“ ℓₐ β„“α΅£} {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:

Poset[_,_]
  : βˆ€ {β„“β‚’ β„“α΅£ β„“β‚’' β„“α΅£'}
  β†’ (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:

Posets-has-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