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 β-categoryβ (as opposed to a β-categoryβ), 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) β¦
(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')