Powersets
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Louis Wasserman, Maša Žaucer and Gregor Perčič.
Created on 2022-04-21.
Last modified on 2025-02-08.
module foundation.powersets where
Imports
open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.empty-types open import foundation.identity-types open import foundation.large-locale-of-propositions open import foundation.logical-equivalences open import foundation.propositions open import foundation.subtypes open import foundation.unit-type open import foundation.universe-levels open import foundation-core.sets open import order-theory.bottom-elements-large-posets open import order-theory.bottom-elements-posets open import order-theory.dependent-products-large-meet-semilattices open import order-theory.dependent-products-large-posets open import order-theory.dependent-products-large-preorders open import order-theory.dependent-products-large-suplattices open import order-theory.large-meet-semilattices open import order-theory.large-posets open import order-theory.large-preorders open import order-theory.large-suplattices open import order-theory.meet-semilattices open import order-theory.order-preserving-maps-large-posets open import order-theory.order-preserving-maps-large-preorders open import order-theory.posets open import order-theory.preorders open import order-theory.similarity-of-elements-large-posets open import order-theory.suplattices open import order-theory.top-elements-large-posets open import order-theory.top-elements-posets
Idea
The powerset¶ of a type is the set of all subtypes.
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) powerset-Large-Preorder = Π-Large-Preorder {I = A} (λ _ → Prop-Large-Preorder) module _ {l1 : Level} (l2 : Level) (A : UU l1) where powerset-Preorder : Preorder (l1 ⊔ lsuc l2) (l1 ⊔ l2) powerset-Preorder = preorder-Large-Preorder (powerset-Large-Preorder A) l2
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) powerset-Large-Poset = Π-Large-Poset {I = A} (λ _ → Prop-Large-Poset) module _ {l1 : Level} (l2 : Level) (A : UU l1) where powerset-Poset : Poset (l1 ⊔ lsuc l2) (l1 ⊔ l2) powerset-Poset = poset-Large-Poset (powerset-Large-Poset A) l2
The powerset poset has a top element
module _ {l1 : Level} (A : UU l1) where has-top-element-powerset-Large-Poset : has-top-element-Large-Poset (powerset-Large-Poset A) has-top-element-powerset-Large-Poset = has-top-element-Π-Large-Poset ( λ _ → Prop-Large-Poset) ( λ _ → has-top-element-Prop-Large-Locale) has-top-element-powerset-Poset : {l2 : Level} → has-top-element-Poset (powerset-Poset l2 A) has-top-element-powerset-Poset {l2} = (λ _ → raise-unit-Prop l2) , (λ _ _ _ → raise-star)
The powerset poset has a bottom element
module _ {l1 : Level} (A : UU l1) where has-bottom-element-powerset-Large-Poset : has-bottom-element-Large-Poset (powerset-Large-Poset A) has-bottom-element-powerset-Large-Poset = has-bottom-element-Π-Large-Poset ( λ _ → Prop-Large-Poset) ( λ _ → has-bottom-element-Prop-Large-Locale) has-bottom-element-powerset-Poset : {l2 : Level} → has-bottom-element-Poset (powerset-Poset l2 A) has-bottom-element-powerset-Poset {l2} = (λ _ → raise-empty-Prop l2) , (λ _ _ → raise-ex-falso l2)
The powerset meet semilattice
module _ {l1 : Level} (A : UU l1) where powerset-Large-Meet-Semilattice : Large-Meet-Semilattice (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3) powerset-Large-Meet-Semilattice = Π-Large-Meet-Semilattice {I = A} (λ _ → Prop-Large-Meet-Semilattice)
The powerset suplattice
module _ {l1 : Level} (A : UU l1) where powerset-Large-Suplattice : Large-Suplattice (λ l2 → lsuc l2 ⊔ l1) (λ l2 l3 → l2 ⊔ l3 ⊔ l1) lzero powerset-Large-Suplattice = Π-Large-Suplattice {I = A} (λ _ → Prop-Large-Suplattice) powerset-Suplattice : (l2 l3 : Level) → Suplattice (l1 ⊔ lsuc l2 ⊔ lsuc l3) (l1 ⊔ l2 ⊔ l3) l2 powerset-Suplattice = suplattice-Large-Suplattice powerset-Large-Suplattice
Similarity of subtypes
module _ {l1 l2 l3 : Level} {A : UU l1} (P : subtype l2 A) (Q : subtype l3 A) where sim-prop-subtype : Prop (l1 ⊔ l2 ⊔ l3) sim-prop-subtype = sim-prop-Large-Poset (powerset-Large-Poset A) P Q sim-subtype : UU (l1 ⊔ l2 ⊔ l3) sim-subtype = type-Prop sim-prop-subtype has-same-elements-sim-subtype : sim-subtype → has-same-elements-subtype P Q pr1 (has-same-elements-sim-subtype s x) = pr1 s x pr2 (has-same-elements-sim-subtype s x) = pr2 s x sim-has-same-elements-subtype : has-same-elements-subtype P Q → sim-subtype pr1 (sim-has-same-elements-subtype s) x = forward-implication (s x) pr2 (sim-has-same-elements-subtype s) x = backward-implication (s x)
Similarity is reflexive
module _ {l1 : Level} {A : UU l1} where refl-sim-subtype : {l2 : Level} → (P : subtype l2 A) → sim-subtype P P refl-sim-subtype = refl-sim-Large-Poset (powerset-Large-Poset A)
Similarity is transitive
transitive-sim-subtype : {l2 l3 l4 : Level} → (P : subtype l2 A) → (Q : subtype l3 A) → (R : subtype l4 A) → sim-subtype Q R → sim-subtype P Q → sim-subtype P R transitive-sim-subtype = transitive-sim-Large-Poset (powerset-Large-Poset A)
Similarity is antisymmetric at the same universe level
antisymmetric-sim-subtype : {l2 : Level} → (P Q : subtype l2 A) → sim-subtype P Q → P = Q antisymmetric-sim-subtype = eq-sim-Large-Poset (powerset-Large-Poset A)
See also
External links
- Power set at Mathswitch
- power object at Lab
- power set at Lab
- Power set at Wikipedia
Recent changes
- 2025-02-08. Louis Wasserman. Similarity of subtypes is reflexive, transitive, and antisymmetric at the same universe level (#1295).
- 2025-01-07. Fredrik Bakke. Logic (#1226).
- 2024-09-23. Fredrik Bakke. Cantor’s theorem and diagonal argument (#1185).
- 2023-09-21. Egbert Rijke and Gregor Perčič. The classification of cyclic rings (#757).
- 2023-06-09. Fredrik Bakke. Remove unused imports (#648).