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,≀)(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 = 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 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 .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')