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 is the collection of all maps from into the universe of propositional types. Since the universe of all is a (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 : Type β} {S T : β X} β (S β T) β‘ ((x : X) β x β S β x β T)
_ = refl


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 β


## 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

minimal : β X

_β©_ : β X β β X β β 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