open import 1Lab.Prelude

open import Data.Sum

module Data.Power where

private variable
  ℓ : Level
  X : Type ℓ

Power sets🔗

The power set of a type $X$ is the collection of all maps from $X$ into the universe of propositional types. Since the universe of all $n\text{-types}$ is a $(n+1)\text{-type}$ (by n-Type-is-hlevel), and function types have the same h-level as their codomain (by fun-is-hlevel), the power set of a type $X$ is always a set. We denote the power set of $X$ by $\mathbb{P}(X)\text{.}$

ℙ : Type ℓ → Type ℓ
ℙ X = X → Ω

ℙ-is-set : is-set (ℙ X)
ℙ-is-set = hlevel 

The membership relation is defined by applying the predicate and projecting the underlying type of the proposition: We say that $x$ is an element of $P$ if $P(x)$ is inhabited.

_ : ∀ {x : X} {P : ℙ X} → x ∈ P ≡ ∣ P x ∣
_ = refl

The subset relation is defined as is done traditionally: If $x\in X$ implies $x\in Y\text{,}$ for $X,Y:\mathbb{P}(T)\text{,}$ then $X\subseteq Y\text{.}$

_ : {X : Type ℓ} {S T : ℙ X} → (S ⊆ T) ≡ ((x : X) → x ∈ S → x ∈ T)
_ = refl

By function and propositional extensionality, two subsets of $X$ are equal when they contain the same elements, i.e., they assign identical propositions to each inhabitant of $X\text{.}$

ℙ-ext : {A B : ℙ X}
      → A ⊆ B → B ⊆ A → A ≡ B
ℙ-ext {A = A} {B = B} A⊆B B⊂A = funext λ x →
  Ω-ua (A⊆B x) (B⊂A x)

Lattice structure🔗

The type $\mathbb{P}(X)$ has a lattice structure, with the order given by subset inclusion. We call the meets intersections and the joins unions.

maximal : ℙ X
maximal _ = ⊤Ω

minimal : ℙ X
minimal _ = ⊥Ω

_∩_ : ℙ X → ℙ X → ℙ X
(A ∩ B) x = A x ∧Ω B x

_ = ∥_∥
_ = _⊎_

singleton : X → ℙ X
singleton x y = elΩ (x ≡ y)

Note that in the definition of union, we must truncate the coproduct, since there is nothing which guarantees that A and B are disjoint subsets.

_∪_ : ℙ X → ℙ X → ℙ X
(A ∪ B) x = A x ∨Ω B x

infixr  _∩_
infixr  _∪_