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) ⦈
(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) → 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.
Lower-sets-cocomplete : ∀ {ℓ'} {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
Lower-sets-meets : ∀ a b → Meet (Lower-sets P) a b Lower-sets-meets a b .Meet.glb .hom i = (a · i) ∧Ω (b · i) Lower-sets-meets a b .Meet.glb .pres-≤ j≤i (aj , bj) = a .pres-≤ j≤i aj , b .pres-≤ j≤i bj Lower-sets-meets a b .Meet.has-meet .is-meet.meet≤l _ = fst Lower-sets-meets a b .Meet.has-meet .is-meet.meet≤r _ = snd Lower-sets-meets a b .Meet.has-meet .is-meet.greatest lb' f g x x∈lb' = (f x x∈lb') , (g x x∈lb') Lower-sets-joins : ∀ a b → Join (Lower-sets P) a b Lower-sets-joins a b .Join.lub .hom i = (a · i) ∨Ω (b · i) Lower-sets-joins a b .Join.lub .pres-≤ j≤i = ∥-∥-map [ (inl ⊙ a .pres-≤ j≤i) , inr ⊙ b .pres-≤ j≤i ] Lower-sets-joins a b .Join.has-join .is-join.l≤join x x∈a = inc (inl x∈a) Lower-sets-joins a b .Join.has-join .is-join.r≤join x x∈b = inc (inr x∈b) Lower-sets-joins a b .Join.has-join .is-join.least ub' f g x = rec! [ f x , g x ] Lower-sets-top : Top (Lower-sets P) Lower-sets-top .Top.top .hom _ = ⊤Ω Lower-sets-top .Top.top .pres-≤ _ _ = tt Lower-sets-top .Top.has-top _ _ _ = tt Lower-sets-bottom : Bottom (Lower-sets P) Lower-sets-bottom .Bottom.bot .hom _ = ⊥Ω Lower-sets-bottom .Bottom.bot .pres-≤ _ ff = absurd ff Lower-sets-bottom .Bottom.has-bottom _ _ ff = absurd ff
Duality🔗
Lower sets are dual to upper sets.
Lower-sets≅op-Upper-sets : ∀ {o ℓ} (P : Poset o ℓ) → Lower-sets P Posets.≅ (Upper-sets (P ^opp)) Lower-sets≅op-Upper-sets P = Posets.id-iso