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 $(P,\le )$ which does not have all joins, and you want to freely (co)complete it into a poset $P^{\prime }$ which does, along a monotone map $P\to P^{\prime }$ (which additionally preserves meets). To be clear, by a “free cocompletion” we mean that $P^{\prime }$ is the smallest cocomplete poset generated by $P\text{,}$ in that any monotone map $P\to Q$ into a cocomplete poset can be extended uniquely to a cocontinuous monotone map $P^{\prime }\to Q\text{.}$

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 $P$ is a “$\mathbf{Props}\text{-category}$” (as opposed to a “$\mathbf{Sets}\text{-category}$”), then the lower sets of $P$ are precisely the presheaves on $P\text{.}$

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