open import 1Lab.Prelude

open import Data.Sum

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)\bb{P}(X).

β„™ : Type β„“ β†’ Type (lsuc β„“)
β„™ X = X β†’ n-Type _ 1

β„™-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 β†’ Type _
x ∈ P = ∣ P x ∣

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 : \bb{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 β†’
  n-ua {n = 1} (prop-ext (A x .is-tr) (B x .is-tr) (AβŠ†B x) (BβŠ‚A x))

Lattice StructureπŸ”—

The type P(X)\bb{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 _ = Lift _ ⊀ , Ξ» x y i β†’ lift tt

minimal : β„™ X
minimal _ = Lift _ βŠ₯ , Ξ» x β†’ absurd (Lift.lower x)

_∩_ : β„™ X β†’ β„™ X β†’ β„™ X
(A ∩ B) x = (∣ A x ∣ Γ— ∣ B x ∣) , Γ—-is-hlevel 1 (A x .is-tr) (B x .is-tr)

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 ∣ βˆ₯ , squash