open import 1Lab.Prelude open import Data.Sum module Data.Power where

# 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$-types is a $(n+1)$-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 $\bb{P}(X)$.

β : Type β β Type (lsuc β) β X = X β n-Type _ 1 β-is-set : is-set (β X) β-is-set = hlevel 2

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 β Type _ x β P = β£ P x β£

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

_β_ : β X β β X β Type _ X β Y = β x β x β X β x β Y

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

β-ext : {A B : β X} β A β B β B β A β A β‘ B β-ext {A = A} {B = B} AβB BβA = funext Ξ» x β n-ua {n = 1} (prop-ext (A x .is-tr) (B x .is-tr) (AβB x) (BβA x))

## Lattice Structureπ

The type $\bb{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 _ = Lift _ β€ , Ξ» x y i β lift tt minimal : β X minimal _ = Lift _ β₯ , Ξ» x β absurd (Lift.lower x) _β©_ : β X β β X β β X (A β© B) x = (β£ A x β£ Γ β£ B x β£) , Γ-is-hlevel 1 (A x .is-tr) (B x .is-tr)

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 β£ β₯ , squash