open import Cat.Prelude

open import Order.Instances.Pointwise
open import Order.Instances.Props
open import Order.Diagram.Glb
open import Order.Diagram.Lub
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'$ which does, along a monotone map $P \to P'$ (which additionally preserves meets). To be clear, by a “free cocompletion” we mean that $P'$ is the smallest cocomplete poset generated by $P$, in that any monotone map $P \to Q$ into a cocomplete poset can be extended uniquely to a cocontinuous monotone map $P' \to Q$.

Lower-sets : ∀ {ℓₒ ℓᵣ} → Poset ℓₒ ℓᵣ → Poset (ℓₒ ⊔ ℓᵣ) ℓₒ
Lower-sets P = Poset[ (P ^opp) , Props ]

Lower-set : ∀ {ℓₒ ℓᵣ} (P : Poset ℓₒ ℓᵣ) → Type _
Lower-set P = ⌞ Lower-sets 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}$-category” (as opposed to a “$\mathbf{Sets}$-category”), then the lower sets of $P$ are precisely the presheaves on $P$.

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) → Σ _ (is-glb (Lower-sets P) F)
Lower-sets-complete F = fun , glib where
fun : Monotone (P  ^opp) Props
fun .hom i = elΩ (∀ j → i ∈ apply (F j))
fun .pres-≤ y≤x = □-map λ x∈Fj j → F j .pres-≤ y≤x (x∈Fj j)

glib : is-glb (Lower-sets P) F fun
glib .is-glb.glb≤fam i x x∈Fj = (out! x∈Fj) i
glib .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) → Σ _ (is-lub (Lower-sets P) F)
Lower-sets-cocomplete F = fun , lub where
fun : Monotone (P  ^opp) Props
fun .hom i = elΩ (Σ _ λ j → i ∈ apply (F j))
fun .pres-≤ y≤x = □-map λ { (i , x∈Fi) → i , F i .pres-≤ y≤x x∈Fi }

lub : is-lub (Lower-sets P) F fun
lub .is-lub.fam≤lub i x x∈Fi = inc (i , x∈Fi)
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) → Σ _ (is-meet (Lower-sets P) a b)
Lower-sets-meets a b .fst .hom i .∣_∣ = i ∈ (apply a) × i ∈ (apply b )
Lower-sets-meets a b .fst .hom i .is-tr = hlevel!
Lower-sets-meets a b .fst .pres-≤ y≤x (x∈a , x∈b) = (a .pres-≤ y≤x x∈a) , (b .pres-≤ y≤x x∈b)
Lower-sets-meets a b .snd .is-meet.meet≤l _ = fst
Lower-sets-meets a b .snd .is-meet.meet≤r _ = snd
Lower-sets-meets a b .snd .is-meet.greatest lb' f g x x∈lb' = (f x x∈lb') , (g x x∈lb')