module Data.Power where

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 : Type β„“} {x : X} {P Q : β„™ X} β†’ (P βŠ† Q) ≑ (βˆ€ x β†’ x ∈ P β†’ x ∈ Q)
_ = refl

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 _ = ⊀Ω

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 27 _∩_
infixr 26 _βˆͺ_

ImagesπŸ”—

image-of
  : βˆ€ {a b} {A : Type a} {B : Type b} {@(tactic hlevel-tactic-worker) b-set : is-set B}
  β†’ (f : A β†’ B) β†’ β„™ A β†’ β„™ B
∣ image-of {b-set = b-set} f s b ∣ = β–‘ (Ξ£[ a ∈ _ ] ((a ∈ s) Γ— (f a ≑ b)))
image-of {b-set = b-set} f s b .is-tr = squash