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 XX is the collection of all maps from XX into the universe of propositional types. Since the universe of all nn-types is a (n+1)(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 XX is always a set. We denote the power set of XX by P(X)\mathbb{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 xx is an element of PP if P(x)P(x) is inhabited.

_ : βˆ€ {x : X} {P : β„™ X} β†’ x ∈ P ≑ ∣ P x ∣
_ = refl

The subset relation is defined as is done traditionally: If x∈Xx \in X implies x∈Yx \in Y, for X,Y:P(T)X, Y : \mathbb{P}(T), then XβŠ†YX \subseteq Y.

_βŠ†_ : β„™ X β†’ β„™ X β†’ Type _
X βŠ† Y = βˆ€ x β†’ x ∈ X β†’ x ∈ Y

By function and propositional extensionality, two subsets of XX are equal when they contain the same elements, i.e., they assign identical propositions to each inhabitant of XX.

β„™-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)\mathbb{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 _ = el ⊀ hlevel!

minimal : β„™ X
minimal _ = el (Lift _ βŠ₯) hlevel!

_∩_ : β„™ 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 _βˆͺ_