open import Cat.Prelude

open import Order.Instances.Pointwise.Diagrams
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 = Monotone (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 .fst b = elΩ (b P.≤ a)
↓ a .snd x y y<x x<a = P.≤-trans y<x <\$> x<a

よₚ : ⌞ Monotone P (Lower-sets P) ⌟
よₚ .fst = ↓
よₚ .snd x y x<y = (λ a a<x → ⦇ P.≤-trans a<x (pure x<y) ⦈) , tt


## (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 , monotone) , glib where
fun : ⌞ Pointwise ⌞ P ^opp ⌟ Props ⌟
fun i = elΩ (∀ j → i ∈ F j .fst)

monotone : ∀ x y → y P.≤ x → ∣ fun x ∣ → ∣ fun y ∣
monotone x y y<x = □-map λ x∈Fj j → F j .snd x y y<x (x∈Fj j)

glib : is-glb (Lower-sets P) F (fun , monotone)
glib .is-glb.glb≤fam i = (λ x x∈Fj → out! x∈Fj i) , tt
glib .is-glb.greatest lb′ lb′<Fi =
(λ y y∈lb′ → inc (λ j → lb′<Fi j .fst y y∈lb′)) , tt


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 , monotone) , lub where
fun : ⌞ Pointwise ⌞ P ^opp ⌟ Props ⌟
fun i = elΩ (Σ _ λ j → i ∈ F j .fst)

monotone : ∀ x y → y P.≤ x → ∣ fun x ∣ → ∣ fun y ∣
monotone x y y<x = □-map λ { (i , x∈Fi) → i , F i .snd _ _ y<x x∈Fi }

lub : is-lub (Lower-sets P) F (fun , monotone)
lub .is-lub.fam≤lub i = (λ _ i → inc (_ , i)) , tt
lub .is-lub.least lb′ lb′<Fi =
(λ x → □-rec! (λ { (i , x∈Fi) → lb′<Fi i .fst x x∈Fi })) , tt