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 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 = 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 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 .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