open import Cat.Prelude

open import Data.Power hiding (_β©_ ; _βͺ_)

open import Order.Instances.Pointwise
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.Base

module Order.Instances.Pointwise.Diagrams where


# Pointwise joins and meetsπ

This module establishes that joins and meets are a pointwise construction, in the following sense: Suppose that and are families of elements with a poset, such that, for all we have 1, then when is given the pointwise ordering.

module _ {ββ βα΅£ βα΅’} {I : Type βα΅’} {P : I β Poset ββ βα΅£} where
private module P {i} = Poset (P i)

is-top-pointwise
: β {t} (pt : β i β is-top (P i) (t i))
β is-top (Pointwise I P) t
is-top-pointwise pt fam i = pt i (fam i)

has-top-pointwise
: (β i β Top (P i))
β Top (Pointwise I P)
has-top-pointwise pt .Top.top i = pt i .Top.top
has-top-pointwise pt .Top.has-top = is-top-pointwise Ξ» i β pt i .Top.has-top

is-bottom-pointwise
: β {b} (pt : β i β is-bottom (P i) (b i))
β is-bottom (Pointwise I P) b
is-bottom-pointwise pb fam i = pb i (fam i)

has-bottom-pointwise
: (β i β Bottom (P i))
β Bottom (Pointwise I P)
has-bottom-pointwise pt .Bottom.bot i = pt i .Bottom.bot
has-bottom-pointwise pt .Bottom.has-bottom =
is-bottom-pointwise Ξ» i β pt i .Bottom.has-bottom

is-meet-pointwise
: β {f g h} (pms : β i β is-meet (P i) (f i) (g i) (h i))
β is-meet (Pointwise I P) f g h
is-meet-pointwise pwise .is-meet.meetβ€l i = pwise i .is-meet.meetβ€l
is-meet-pointwise pwise .is-meet.meetβ€r i = pwise i .is-meet.meetβ€r
is-meet-pointwise pwise .is-meet.greatest lb' lb'<f lb'<g i =
pwise i .is-meet.greatest (lb' i) (lb'<f i) (lb'<g i)

is-join-pointwise
: β {f g h} (pjs : β i β is-join (P i) (f i) (g i) (h i))
β is-join (Pointwise I P) f g h
is-join-pointwise pwise .is-join.lβ€join i = pwise i .is-join.lβ€join
is-join-pointwise pwise .is-join.rβ€join i = pwise i .is-join.rβ€join
is-join-pointwise pwise .is-join.least lb' lb'<f lb'<g i =
pwise i .is-join.least (lb' i) (lb'<f i) (lb'<g i)


With a couple more variables, we see that the results above are a special case of both arbitrary lubs and glbs being pointwise:

module
_ {ββ βα΅£ βα΅’ ββ±Ό} {I : Type βα΅’} {J : Type ββ±Ό} {P : J β Poset ββ βα΅£}
(F : I β (j : J) β β P j β)
(m : (j : J) β β P j β)
where

is-lub-pointwise
: (β j β is-lub (P j) (Ξ» i β F i j) (m j))
β is-lub (Pointwise J P) F m
is-lub-pointwise pwise .is-lub.famβ€lub i j = pwise j .is-lub.famβ€lub i
is-lub-pointwise pwise .is-lub.least ub' fi<ub' j =
pwise j .is-lub.least (ub' j) Ξ» i β fi<ub' i j

is-glb-pointwise
: (β j β is-glb (P j) (Ξ» i β F i j) (m j))
β is-glb (Pointwise J P) F m
is-glb-pointwise pwise .is-glb.glbβ€fam i j = pwise j .is-glb.glbβ€fam i
is-glb-pointwise pwise .is-glb.greatest ub' fi<ub' j =
pwise j .is-glb.greatest (ub' j) Ξ» i β fi<ub' i j

module _ {ββ βα΅£ βα΅’} {I : Type βα΅’} {P : I β Poset ββ βα΅£} where
open is-meet-semilattice

Pointwise-is-meet-slat
: (β a β is-meet-semilattice (P a))
β is-meet-semilattice (Pointwise I P)
Pointwise-is-meet-slat meets ._β©_ x y i = meets i ._β©_ (x i) (y i)
Pointwise-is-meet-slat meets .β©-meets x y = is-meet-pointwise Ξ» a β
meets a .β©-meets (x a) (y a)
Pointwise-is-meet-slat meets .has-top = has-top-pointwise Ξ» a β
meets a .has-top

open is-join-semilattice

Pointwise-is-join-slat
: (β a β is-join-semilattice (P a))
β is-join-semilattice (Pointwise I P)
Pointwise-is-join-slat joins ._βͺ_ x y i = joins i ._βͺ_ (x i) (y i)
Pointwise-is-join-slat joins .βͺ-joins x y = is-join-pointwise Ξ» a β
joins a .βͺ-joins (x a) (y a)
Pointwise-is-join-slat joins .has-bottom = has-bottom-pointwise Ξ» a β
joins a .has-bottom

Subsets-is-meet-slat : β {β} {A : Type β} β is-meet-semilattice (Subsets A)
Subsets-is-meet-slat = Pointwise-is-meet-slat Ξ» _ β Props-is-meet-slat

Subsets-is-join-slat : β {β} {A : Type β} β is-join-semilattice (Subsets A)
Subsets-is-join-slat = Pointwise-is-join-slat Ξ» _ β Props-is-join-slat


Every subset is a least upper bound of singleton sets.

subset-singleton-lub
: β {β} {A : Type β} (P : A β Ξ©)
β is-lub (Subsets A) {I = β«β P} (singleton β fst) P
subset-singleton-lub P .is-lub.famβ€lub (x , xβP) y = rec! Ξ» x=y β subst (_β P) x=y xβP
subset-singleton-lub P .is-lub.least ub singβ€ub x xβP =
singβ€ub (x , xβP) x (inc refl)


1. In the code, this means that is-meet holds, but we will abuse this βfunctionalβ notation for clarity.β©οΈ