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

Created on 2022-04-21.
Last modified on 2023-09-21.

module foundation.powersets where
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


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


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


The powerset is a set

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

  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)

  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)

  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)

  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)

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

Recent changes