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 β†’ Ξ©-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 = 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 _βˆͺ_