module Data.Power where
Power setsπ
The power set of a type
is the collection of all maps from
into the universe of propositional types
. Since the
universe of all
-types
is a
-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
is always a set
. We denote the power set
of
by
.
β : 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 is an element of if is inhabited.
_ : β {x : X} {P : β X} β x β P β‘ β£ P x β£ _ = refl
The subset relation is defined as is done traditionally: If implies , for , then .
_β_ : β X β β X β Type _ X β Y = β x β x β X β x β Y
By function and propositional extensionality, two subsets of are equal when they contain the same elements, i.e., they assign identical propositions to each inhabitant of .
β-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
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 = el (x β A Γ x β B) hlevel!
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 = elΞ© (x β A β x β B) infixr 22 _β©_ infixr 21 _βͺ_