module Order.Instances.Lower where

Lower setsπŸ”—

Imagine you have a poset which does not have all joins, and you want to freely (co)complete it into a poset which does, along a monotone map (which additionally preserves meets). To be clear, by a β€œfree cocompletion” we mean that is the smallest cocomplete poset generated by in that any monotone map into a cocomplete poset can be extended uniquely to a cocontinuous monotone map

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 is a β€œβ€ (as opposed to a β€œβ€), then the lower sets of are precisely the presheaves on

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) ⦈


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:

    : βˆ€ {β„“'} {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.

    : βˆ€ {β„“'} {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