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 XX can be organised into a lattice, where the meets of two subsets are given by their intersection x∩yx \cap y and the joins are given by their union xβˆͺyx \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))
    Ξ» {x} {y} β†’ hlevel!

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

∩-semilattice : βˆ€ {β„“} {X : Type β„“} β†’ is-semilattice (_∩_ {X = X})
∩-semilattice = r where
  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 P(X),∩,βˆͺ\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 ._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)↔(x≑(x∩y))(x βŠ† y) \leftrightarrow (x ≑ (x ∩ y)).

subset-∩ : βˆ€ {β„“} {A : Type β„“} {X Y : β„™ A} β†’ (X βŠ† Y) ≃ (X ≑ (X ∩ Y))
subset-∩ {X = X} {Y = Y} =
  prop-ext (hlevel!) (β„™-is-set _ _) to from

In the β€œif” direction, suppose that XβŠ†YX \subseteq Y. We show that X∩YX ∩ Y intersects to XX by extensionality of power sets: If x∈Xx \in X and XβŠ†YX \subseteq Y then x∈Yx \in Y, so x∈(X∩Y)x \in (X \cap Y). Conversely, if x∈(X∩Y)x \in (X \cap Y), then x∈Xx \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)
                   (Ξ» x x∈X∩Y β†’ x∈X∩Y .fst)

In the β€œonly if” direction, suppose that X=(X∩Y)X = (X \cap Y). If x∈Xx \in X, then x∈(X∩Y)x \in (X \cap Y) (by the assumed equality), so x∈Yx \in Y, hence XβŠ†YX \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


The lattice of powersets of a type is complete, since it admits arbitrary meets. The meet of a family F:Iβ†’PF : I \to \bb{P} is the subset represented by {i:(βˆ€x)Β i∈F(x)}\{ 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

    : βˆ€ {I : Type β„“} (F : I β†’ β„™ X)
    β†’ Indexed-product β„™.underlying F
  β„™-indexed-meet F = ip where
    ip : Indexed-product _ _
    ip .Ξ F i      = el! (βˆ€ x β†’ i ∈ F x)
    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 FF is like above, by the subset {i:(βˆƒx)Β i∈F(x)}\{ i : (\exists x)\ i \in F(x) \}. Note the use of βˆƒ\exists, rather than βˆ‘\sum: we need a proposition.

  open Indexed-coproduct

    : βˆ€ {I : Type β„“} (F : I β†’ β„™ X)
    β†’ Indexed-coproduct β„™.underlying F
  β„™-indexed-join F = ic where
    ic : Indexed-coproduct _ _
    ic .Ξ£F i      = el (βˆƒ[ 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}