Powersets

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Maša Žaucer and Gregor Perčič.

Created on 2022-04-21.
Last modified on 2024-09-23.

module foundation.powersets where
Imports 
open import foundation.subtypes
open import foundation.universe-levels

open import foundation-core.sets

open import order-theory.large-posets
open import order-theory.large-preorders
open import order-theory.posets
open import order-theory.preorders

Idea

The powerset of a type is the set of all subtypes with respect to a given universe level.

Definition

powerset :
  {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
powerset = subtype

Properties

The powerset is a set

module _
  {l1 : Level} (A : UU l1)
  where

  is-set-powerset : {l2 : Level} → is-set (powerset l2 A)
  is-set-powerset = is-set-subtype

  powerset-Set : (l2 : Level) → Set (l1 ⊔ lsuc l2)
  powerset-Set l2 = subtype-Set l2 A

The powerset large preorder

module _
  {l1 : Level} (A : UU l1)
  where

  powerset-Large-Preorder :
    Large-Preorder (λ l → l1 ⊔ lsuc l) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
  type-Large-Preorder powerset-Large-Preorder l = subtype l A
  leq-prop-Large-Preorder powerset-Large-Preorder = leq-prop-subtype
  refl-leq-Large-Preorder powerset-Large-Preorder = refl-leq-subtype
  transitive-leq-Large-Preorder powerset-Large-Preorder = transitive-leq-subtype

The powerset large poset

module _
  {l1 : Level} (A : UU l1)
  where

  powerset-Large-Poset :
    Large-Poset (λ l → l1 ⊔ lsuc l) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
  large-preorder-Large-Poset powerset-Large-Poset = powerset-Large-Preorder A
  antisymmetric-leq-Large-Poset powerset-Large-Poset P Q =
    antisymmetric-leq-subtype P Q

The powerset preorder at a universe level

module _
  {l1 : Level} (A : UU l1)
  where

  powerset-Preorder : (l2 : Level) → Preorder (l1 ⊔ lsuc l2) (l1 ⊔ l2)
  powerset-Preorder = preorder-Large-Preorder (powerset-Large-Preorder A)

The powerset poset at a universe level

module _
  {l1 : Level} (A : UU l1)
  where

  powerset-Poset : (l2 : Level) → Poset (l1 ⊔ lsuc l2) (l1 ⊔ l2)
  powerset-Poset = poset-Large-Poset (powerset-Large-Poset A)

Recent changes