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