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
$P(X).$

β : Type β β Type β β X = X β Ξ© β-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} {P : β X} β x β P β‘ β£ P x β£ _ = refl

The **subset** relation is defined as is done
traditionally: If
$xβX$
implies
$xβY,$
for
$X,Y:P(T),$
then
$XβY.$

_ : {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.$

β-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
$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 32 _β©_ infixr 31 _βͺ_