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,≀)(P, \le) which does not have all joins, and you want to freely (co)complete it into a poset Pβ€²P' which does, along a monotone map Pβ†’Pβ€²P \to P' (which additionally preserves meets). To be clear, by a β€œfree cocompletion” we mean that Pβ€²P' is the smallest cocomplete poset generated by PP, in that any monotone map Pβ†’QP \to Q into a cocomplete poset can be extended uniquely to a cocontinuous monotone map Pβ€²β†’QP' \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 PP is a β€œProps{{\mathbf{Props}}}-category” (as opposed to a β€œSets{{\mathbf{Sets}}}-category”), then the lower sets of PP are precisely the presheaves on PP.

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