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