open import Cat.Prelude

open import Data.Sum.Base

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

import Order.Reasoning as Pr

module Order.Instances.Lower where


# Lower setsπ

Imagine you have a poset which does not have all joins, and you want to freely (co)complete it into a poset which does, along a monotone map (which additionally preserves meets). To be clear, by a βfree cocompletionβ we mean that is the smallest cocomplete poset generated by in that any monotone map into a cocomplete poset can be extended uniquely to a cocontinuous monotone map

Lower-sets : β {ββ βα΅£} β Poset ββ βα΅£ β Poset (ββ β βα΅£) ββ
Lower-sets P = Poset[ (P ^opp) , Props ]

Lower-set : β {ββ βα΅£} (P : Poset ββ βα΅£) β Type _
Lower-set P = β Lower-sets P β

module _ {ββ βα΅£} {P : Poset ββ βα΅£} where
private module P = Pr P


Note the similarity between this construction and the Yoneda embedding: Indeed, if we take the perspective that a poset is a ββ (as opposed to a ββ), then the lower sets of are precisely the presheaves on

module _ {ββ βα΅£} (P : Poset ββ βα΅£) where
private module P = Pr P

β : β P β β Lower-set P
β a .hom b = elΞ© (b P.β€ a)
β a .pres-β€ y<x x<a = P.β€-trans y<x <\$> x<a

γβ : Monotone P (Lower-sets P)
γβ .hom = β
γβ .pres-β€ xβ€y a aβ€x = β¦ P.β€-trans aβ€x (pure xβ€y) β¦


## (Co)completenessπ

Let us first show that the poset of lower sets is cocomplete (and complete), in that it admits all meets and joins. The meet of a family of lower sets is given by the product of the underlying propositions. Because propositional resizing, we can create meets of families indexed by arbitrarily large types:

  Lower-sets-complete
: β {β'} {I : Type β'} (F : I β Lower-set P) β Glb (Lower-sets P) F
Lower-sets-complete F .Glb.glb .hom i = elΞ© (β j β i β F j)
Lower-sets-complete F .Glb.glb .pres-β€ jβ€i =
β‘-map Ξ» xβFj j β F j .pres-β€ jβ€i (xβFj j)
Lower-sets-complete F .Glb.has-glb .is-glb.glbβ€fam i x xβFj = β‘-out! xβFj i
Lower-sets-complete F .Glb.has-glb .is-glb.greatest lb' lb'β€Fi x yβlb' =
inc (Ξ» j β lb'β€Fi j x yβlb')


The same thing happens for joins, which are given by an existential quantifier. Note that we directly resize a sigma, because our resizing operator automatically propositionally truncates.

  Lower-sets-cocomplete
: β {β'} {I : Type β'} (F : I β Lower-set P) β Lub (Lower-sets P) F
Lower-sets-cocomplete {I = I} F .Lub.lub .hom i =
elΞ© (Ξ£[ j β I ] i β F j)
Lower-sets-cocomplete F .Lub.lub .pres-β€ jβ€i =
β‘-map Ξ» { (i , xβFi) β i , F i .pres-β€ jβ€i xβFi }
Lower-sets-cocomplete F .Lub.has-lub .is-lub.famβ€lub i x xβFi =
inc (i , xβFi)
Lower-sets-cocomplete F .Lub.has-lub .is-lub.least lb' lb'β€Fi x =
rec! Ξ» i xβFi β lb'β€Fi i x xβFi

  Lower-sets-meets : (a b : Lower-set P) β Meet (Lower-sets P) a b
Lower-sets-meets a b .Meet.glb .hom i = (a # i) β§Ξ© (b # i)
Lower-sets-meets a b .Meet.glb .pres-β€ jβ€i (aj , bj) =
a .pres-β€ jβ€i aj , b .pres-β€ jβ€i bj
Lower-sets-meets a b .Meet.has-meet .is-meet.meetβ€l _ = fst
Lower-sets-meets a b .Meet.has-meet .is-meet.meetβ€r _ = snd
Lower-sets-meets a b .Meet.has-meet .is-meet.greatest lb' f g x xβlb' =
(f x xβlb') , (g x xβlb')

Lower-sets-joins : (a b : Lower-set P) β Join (Lower-sets P) a b
Lower-sets-joins a b .Join.lub .hom i = (a # i) β¨Ξ© (b # i)
Lower-sets-joins a b .Join.lub .pres-β€ jβ€i =
β₯-β₯-map [ (inl β a .pres-β€ jβ€i) , inr β b .pres-β€ jβ€i ]
Lower-sets-joins a b .Join.has-join .is-join.lβ€join x xβa = inc (inl xβa)
Lower-sets-joins a b .Join.has-join .is-join.rβ€join x xβb = inc (inr xβb)
Lower-sets-joins a b .Join.has-join .is-join.least ub' f g x =
rec! [ f x , g x ]

Lower-sets-top : Top (Lower-sets P)
Lower-sets-top .Top.top .hom _ = β€Ξ©
Lower-sets-top .Top.top .pres-β€ _ _ = tt
Lower-sets-top .Top.has-top _ _ _ = tt

Lower-sets-bottom : Bottom (Lower-sets P)
Lower-sets-bottom .Bottom.bot .hom _ = β₯Ξ©
Lower-sets-bottom .Bottom.bot .pres-β€ _ ff = absurd ff
Lower-sets-bottom .Bottom.has-bottom _ _ ff = absurd ff