open import 1Lab.Prelude

open import Algebra.Semilattice
open import Algebra.Semigroup
open import Algebra.Lattice
open import Algebra.Magma

open import Cat.Diagram.Coproduct.Indexed
open import Cat.Diagram.Product.Indexed
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Limit.Base
open import Cat.Thin.Limits
open import Cat.Thin

open import Data.Power
open import Data.Sum

module Data.Power.Lattice where


# Lattice of Subobjectsπ

The power set of a type $X$ can be organised into a lattice, where the meets of two subsets are given by their intersection $x \cap y$ and the joins are given by their union $x \cup y$. Furthermore, we prove that the ordering induced by this lattice is the same as the subset inclusion ordering.

First, we take a detour to define the structure of β as a Poset ordered by subset inclusion. This packages up the reflexivity and transitivity of the subset relation. Antisymmetry for this relation is exactly the principle of extensionality for subsets.

ββ : β {β} β Type β β Poset _ _
ββ A =
make-poset {A = β A} {R = _β_}
(Ξ» _ x β x)
(Ξ» xβy yβz a aβx β yβz a (xβy a aβx))
β-ext
Ξ» {x} {y} β Ξ -is-hlevel 1 Ξ» x β fun-is-hlevel 1 (y x .is-tr)


Back on track, we equip intersection of subsets with the structure of a semilattice:

β©-semilattice : β {β} {X : Type β} β is-semilattice (_β©_ {X = X})
open is-semilattice
open is-semigroup

r : is-semilattice _
r .has-is-semigroup .has-is-magma .has-is-set = β-is-set
r .has-is-semigroup .associative =
β-ext (Ξ» { x (a , b , c) β (a , b) , c })
(Ξ» { x ((a , b) , c) β a , b , c })

r .commutative =
β-ext (Ξ» { x (a , b) β b , a }) (Ξ» { x (a , b) β b , a })

r .idempotent =
β-ext (Ξ» { x (y , _) β y }) (Ξ» { x y β y , y })


We then equip union of subsets with the structure of a semilattice. This direction of the proof is a lot more annoying because of the truncation in _βͺ_, but it is essentially shuffling sums around:

βͺ-semilattice : β {β} {X : Type β} β is-semilattice (_βͺ_ {X = X})
βͺ-semilattice = r where
open is-semilattice
open is-semigroup


To show that subset union is associative, we must βshuffleβ coproducts (x β X) β (x β Y β x β Z) to (x β X β x β Y) β (x β Z), which would be simple enough to do with pattern matching. The complication arises because in reality weβre shuffling P β β₯ Q β R β₯ into β₯ P β Q β₯ β R and vice-versa, so we must use β₯-β₯-elim to get at the underlying coproduct, even though all of P, Q, and R are propositions.

  r : is-semilattice _
r .has-is-semigroup .has-is-magma .has-is-set = β-is-set
r .has-is-semigroup .associative =
β-ext (Ξ» _ β β₯-β₯-elim (Ξ» _ β squash)
Ξ» { (inl x) β inc (inl (inc (inl x)))
; (inr x) β β₯-β₯-elim (Ξ» _ β squash)
(Ξ» { (inl y) β inc (inl (inc (inr y)))
; (inr y) β inc (inr y) }) x
})
(Ξ» _ β β₯-β₯-elim (Ξ» _ β squash)
Ξ» { (inl x) β β₯-β₯-elim (Ξ» _ β squash)
(Ξ» { (inl y) β inc (inl y)
; (inr y) β inc (inr (inc (inl y))) }) x
; (inr x) β inc (inr (inc (inr x)))
})


For commutativity, since we are changing β₯ (x β X) β (x β Y) β₯ to β₯ (x β Y) β (x β X) β₯, β΅β₯-β₯-map{.Agda} suffices - there is no need to reassociate truncations.

  r .commutative =
β-ext (Ξ» _ β β₯-β₯-map Ξ» { (inl x) β inr x
; (inr x) β inl x })
(Ξ» _ β β₯-β₯-map Ξ» { (inl x) β inr x
; (inr x) β inl x })


For idempotence, we must show that x β X β β₯ (x β X) β (x β X) β₯. Since x β X is a proposition, we can eliminate from a truncation to it, at which point either branch will do just fine. In the other direction, we inject it into the left summand for definiteness.

  r .idempotent {x = X} =
β-ext (Ξ» _ β β₯-β₯-elim (Ξ» _ β X _ .is-tr)
(Ξ» { (inl x) β x
; (inr x) β x }))
Ξ» _ x β inc (inl x)


We must now show that intersections absorb unions, and that unions absorb intersections.

β©-absorbs-βͺ : β {β} {A : Type β} {X Y : β A} β X β© (X βͺ Y) β‘ X
β©-absorbs-βͺ = β-ext (Ξ» { _ (a , _) β a }) Ξ» _ x β x , inc (inl x)

βͺ-absorbs-β© : β {β} {A : Type β} {X Y : β A} β X βͺ (X β© Y) β‘ X
βͺ-absorbs-β© {X = X} {Y = Y} =
β-ext (Ξ» _ β β₯-β₯-elim (Ξ» x β X _ .is-tr)
(Ξ» { (inl xβX) β xβX
; (inr (xβX , xβY)) β xβX }))
Ξ» _ xβX β inc (inl xβX)


This means that $\bb{P}(X), \cap, \cup$ assemble into a lattice, which we call Power:

open Lattice-on
open is-lattice

Power : β {β} (X : Type β) β Lattice-on (β X)
Power X ._Lβ¨_ = _βͺ_
Power X .has-is-lattice .has-meets = β©-semilattice
Power X .has-is-lattice .has-joins = βͺ-semilattice
Power X .has-is-lattice .β§-absorbs-β¨ {y = y} = β©-absorbs-βͺ {Y = y}
Power X .has-is-lattice .β¨-absorbs-β§ {y = y} = βͺ-absorbs-β© {Y = y}


It remains to show that the covariant ordering induced by the Power lattice is the same as ββ. For this we show that $(x β y) \leftrightarrow (x β‘ (x β© y))$.

subset-β© : β {β} {A : Type β} {X Y : β A} β (X β Y) β (X β‘ (X β© Y))
subset-β© {X = X} {Y = Y} =
prop-ext
(Ξ -is-hlevel 1 Ξ» x β fun-is-hlevel 1 (Y x .is-tr))
(β-is-set _ _)
to from
where


In the βifβ direction, suppose that $X \subseteq Y$. We show that $X β© Y$ intersects to $X$ by extensionality of power sets: If $x \in X$ and $X \subseteq Y$ then $x \in Y$, so $x \in (X \cap Y)$. Conversely, if $x \in (X \cap Y)$, then $x \in X$, so we are done.

    to : X β Y β X β‘ (X β© Y)
to xβy = β-ext (Ξ» x xβX β xβX , xβy x xβX)


In the βonly ifβ direction, suppose that $X = (X \cap Y)$. If $x \in X$, then $x \in (X \cap Y)$ (by the assumed equality), so $x \in Y$, hence $X \subseteq Y$, so we are done.

    from : (X β‘ (X β© Y)) β X β Y
from path x xβX = transport (ap β£_β£ (happly path x)) xβX .snd


## Completenessπ

The lattice of powersets of a type is complete, since it admits arbitrary meets. The meet of a family $F : I \to \bb{P}$ is the subset represented by $\{ i : (\forall x)\ i \in F(x) \}$, i.e., the set of elements present in all the subsets in the family.

module _ {β} {X : Type β} where
private module β = Poset (ββ X)
open Indexed-product

β-indexed-meet
: β {I : Type β} (F : I β β X)
β Indexed-product β.underlying F
β-indexed-meet F = ip where
ip : Indexed-product _ _
ip .Ξ F i      = (β x β i β F x) , Ξ -is-hlevel 1 Ξ» x β F x i .is-tr
ip .Ο i x f   = f i
ip .has-is-ip = indexed-meetβindexed-product {P = β.βProset} _
Ξ» f x b i β f i x b

β-complete : is-complete β β β.underlying
β-complete = has-indexed-productsβproset-is-complete {P = β.βProset} β-indexed-meet


It is also cocomplete, since it admits arbitrary indexed joins. These are given, assuming $F$ is like above, by the subset $\{ i : (\exists x)\ i \in F(x) \}$. Note the use of $\exists$, rather than $\sum$: we need a proposition.

  open Indexed-coproduct

β-indexed-join
: β {I : Type β} (F : I β β X)
β Indexed-coproduct β.underlying F
β-indexed-join F = ic where
ic : Indexed-coproduct _ _
ic .Ξ£F i      = (β[ x β _ ] (i β F x)) , squash
ic .ΞΉ i x f   = inc (i , f)
ic .has-is-ic = indexed-joinβindexed-coproduct {P = β.βProset} _
Ξ» {B = B} f x β β₯-β₯-elim (Ξ» _ β B x .is-tr) (Ξ» { (i , y) β f i x y })

β-cocomplete : is-cocomplete β β β.underlying
β-cocomplete = has-indexed-coproductsβproset-is-cocomplete {P = β.βProset}
β-indexed-join
`