From 10c161268d1c8f5c6e77279d049eb596baec7033 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 9 Oct 2024 21:15:38 +0200 Subject: [PATCH] Idea text `set-theory` (#1189) Adds an idea text to `set-theory`. Comments are very welcome! Also, moves Russel's paradox to the `set-theory` namespace, fixes some typographical things, and adds a few number sequences for some reason. --- references.bib | 34 ++++++- .../falling-factorials.lagda.md | 4 +- .../multiset-coefficients.lagda.md | 20 +++- .../peano-arithmetic.lagda.md | 13 ++- src/foundation.lagda.md | 1 - src/foundation/axiom-of-choice.lagda.md | 8 +- src/foundation/connected-maps.lagda.md | 8 +- .../multivariable-correspondences.lagda.md | 2 +- src/foundation/singleton-subtypes.lagda.md | 4 +- src/foundation/small-universes.lagda.md | 6 +- .../truncation-equivalences.lagda.md | 8 +- src/graph-theory/polygons.lagda.md | 2 +- src/group-theory/dihedral-groups.lagda.md | 4 +- .../oeis.lagda.md | 30 ++++++ src/set-theory.lagda.md | 44 +++++++++ .../russells-paradox.lagda.md | 94 ++++++++++--------- src/trees/multisets.lagda.md | 5 +- src/trees/small-multisets.lagda.md | 11 ++- src/trees/universal-multiset.lagda.md | 6 +- .../presented-pi-finite-types.lagda.md | 6 +- 20 files changed, 219 insertions(+), 91 deletions(-) rename src/{foundation => set-theory}/russells-paradox.lagda.md (59%) diff --git a/references.bib b/references.bib index dbb074617f..c187b5558f 100644 --- a/references.bib +++ b/references.bib @@ -52,11 +52,11 @@ @online{BdJR24 } @phdthesis{Booij20PhD, - title = {Analysis in univalent type theory}, - author = {Booij, Auke Bart}, - year = {2020}, - school = {University of Birmingham}, - url = {https://etheses.bham.ac.uk/id/eprint/10411/7/Booij20PhD.pdf} + title = {Analysis in univalent type theory}, + author = {Booij, Auke Bart}, + year = {2020}, + school = {University of Birmingham}, + url = {https://etheses.bham.ac.uk/id/eprint/10411/7/Booij20PhD.pdf} } @book{BSCS05, @@ -260,6 +260,19 @@ @article{Esc21 keywords = {55U40 03B15,Mathematics - Algebraic Geometry,Mathematics - Logic} } +@book{FBL73, + author = {Fraenkel, Abraham A. and Bar-Hillel, Yehoshua and Levy, + Azriel}, + title = {Foundations of set theory}, + series = {Studies in Logic and the Foundations of Mathematics}, + volume = {67}, + edition = {revised}, + note = {With the collaboration of Dirk van Dalen}, + publisher = {North-Holland Publishing Co., Amsterdam-London}, + year = {1973}, + pages = {x+404} +} + @online{Felixwellen/DCHoTT-Agda, title = {Felixwellen/{{DCHoTT-Agda}}}, author = {Cherubini, Felix}, @@ -300,6 +313,17 @@ @article{KECA17 eprintclass = {cs} } +@book{Kunen11, + author = {Kunen, Kenneth}, + title = {Set theory}, + series = {Studies in Logic (London)}, + volume = {34}, + publisher = {College Publications, London}, + year = {2011}, + pages = {viii+401}, + isbn = {978-1-84890-050-9} +} + @inproceedings{KvR19, title = {{Path Spaces of Higher Inductive Types in Homotopy Type Theory}}, booktitle = {Proceedings of the 34th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}}}, diff --git a/src/elementary-number-theory/falling-factorials.lagda.md b/src/elementary-number-theory/falling-factorials.lagda.md index 9184af7e76..10cf292907 100644 --- a/src/elementary-number-theory/falling-factorials.lagda.md +++ b/src/elementary-number-theory/falling-factorials.lagda.md @@ -15,7 +15,9 @@ open import elementary-number-theory.natural-numbers ## Idea -The falling factorial (n)\_m is the number n(n-1)⋯(n-m+1) +The +{{#concept "falling factorial" WD="falling and rising factorial" WDID=Q2339261 Agda=falling-factorial-ℕ}} +`(n)ₘ` is the number `n(n-1)⋯(n-m+1)`. ## Definition diff --git a/src/elementary-number-theory/multiset-coefficients.lagda.md b/src/elementary-number-theory/multiset-coefficients.lagda.md index 211771b40d..714dfa905c 100644 --- a/src/elementary-number-theory/multiset-coefficients.lagda.md +++ b/src/elementary-number-theory/multiset-coefficients.lagda.md @@ -15,14 +15,26 @@ open import elementary-number-theory.natural-numbers ## Idea -The multiset coefficients count the number of multisets of size `k` of elements -of a set of size `n`. In oter words, it counts the number of connected componets -of the type +The multiset coefficients count the number of [multisets](trees.multisets.md) of +size `k` of elements of a [set](foundation-core.sets.md) of size `n`. In other +words, it counts the number of +[connected componets](foundation.connected-components.md) of the type ```text - Σ (A : Fin n → 𝔽), ∥ Fin k ≃ Σ (i : Fin n), A i ∥. + Σ (A : Fin n → 𝔽), ║ Fin k ≃ Σ (i : Fin n), A i ║. ``` +The first few numbers are + +| n\k | 0 | 1 | 2 | 3 | 4 | 5 | +| :---: | --: | --: | --: | --: | --: | --: | +| **0** | 1 | 0 | 0 | 0 | 0 | 0 | +| **1** | 1 | 1 | 1 | 1 | 1 | 1 | +| **2** | 1 | 2 | 3 | 4 | 5 | 6 | +| **3** | 1 | 3 | 6 | 10 | 15 | 21 | +| **4** | 1 | 4 | 10 | 20 | 35 | 56 | +| **5** | 1 | 5 | 15 | 35 | 70 | 126 | + ## Definition ```agda diff --git a/src/elementary-number-theory/peano-arithmetic.lagda.md b/src/elementary-number-theory/peano-arithmetic.lagda.md index db068185b2..25e87794d3 100644 --- a/src/elementary-number-theory/peano-arithmetic.lagda.md +++ b/src/elementary-number-theory/peano-arithmetic.lagda.md @@ -22,9 +22,9 @@ open import foundation.universe-levels ## Axioms -We state the Peano axioms in type theory, using the -[identity type](foundation-core.identity-types.md) as equality, and prove that -they hold for the +We state the {{#concept "Peano axioms" WD="Peano axioms" WDID=Q842755}} in type +theory using the [identity type](foundation-core.identity-types.md) as equality, +and prove that they hold for the [natural numbers `ℕ`](elementary-number-theory.natural-numbers.md). ### Peano's 1st axiom @@ -39,7 +39,7 @@ peano-1-ℕ : peano-axiom-1 ℕ peano-1-ℕ = zero-ℕ ``` -## Peano's 2nd axiom +### Peano's 2nd axiom The identity relation on the natural numbers is reflexive. I.e. for every natural number `x`, it is true that `x ＝ x`. @@ -67,8 +67,8 @@ peano-3-ℕ x y = inv ### Peano's 4th axiom -The identity relation on the natural numbers is transitive. I.e. if `y ＝ z` and -`x ＝ y`, then `x ＝ z`. +The identity relation on the natural numbers is transitive. I.e., if `y ＝ z` +and `x ＝ y`, then `x ＝ z`. ```agda peano-axiom-4 : {l : Level} → UU l → UU l @@ -156,7 +156,6 @@ peano-9-ℕ P = ind-ℕ {P = type-Prop ∘ P} ## External links - [Peano arithmetic](https://ncatlab.org/nlab/show/Peano+arithmetic) at $n$Lab -- [Peano axioms](https://www.wikidata.org/wiki/Q842755) at Wikidata - [Peano axioms](https://www.britannica.com/science/Peano-axioms) at Britannica - [Peano axioms](https://en.wikipedia.org/wiki/Peano_axioms) at Wikipedia - [Peano's Axioms](https://mathworld.wolfram.com/PeanosAxioms.html) at Wolfram diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index b892a43bab..83228240ab 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -340,7 +340,6 @@ open import foundation.replacement public open import foundation.retractions public open import foundation.retracts-of-maps public open import foundation.retracts-of-types public -open import foundation.russells-paradox public open import foundation.sections public open import foundation.separated-types public open import foundation.sequences public diff --git a/src/foundation/axiom-of-choice.lagda.md b/src/foundation/axiom-of-choice.lagda.md index a7bd0fea94..319776bde7 100644 --- a/src/foundation/axiom-of-choice.lagda.md +++ b/src/foundation/axiom-of-choice.lagda.md @@ -32,10 +32,10 @@ open import foundation-core.sets ## Idea -The {{#concept "axiom of choice" Agda=AC-0}} asserts that for every family of -[inhabited](foundation.inhabited-types.md) types `B` indexed by a -[set](foundation-core.sets.md) `A`, the type of sections of that family -`(x : A) → B x` is inhabited. +The {{#concept "axiom of choice" WD="axiom of choice" WDID=Q179692 Agda=AC-0}} +asserts that for every family of [inhabited](foundation.inhabited-types.md) +types `B` indexed by a [set](foundation-core.sets.md) `A`, the type of sections +of that family `(x : A) → B x` is inhabited. ## Definition diff --git a/src/foundation/connected-maps.lagda.md b/src/foundation/connected-maps.lagda.md index ac66405487..d893f11646 100644 --- a/src/foundation/connected-maps.lagda.md +++ b/src/foundation/connected-maps.lagda.md @@ -335,19 +335,19 @@ is an equivalence for every family `P` of `k`-truncated types. Then it follows that the precomposition function ```text - - ∘ f : ((b : B) → ∥fiber f b∥_k) → ((a : A) → ∥fiber f (f a)∥_k) + - ∘ f : ((b : B) → ║fiber f b║ₖ) → ((a : A) → ║fiber f (f a)║ₖ) ``` is an equivalence. In particular, the element `λ a → η (a , refl)` in the -codomain of this equivalence induces an element `c b : ∥fiber f b∥_k` for each +codomain of this equivalence induces an element `c b : ║fiber f b║ₖ` for each `b : B`. We take these elements as our centers of contraction. Note that by construction, we have an identification `c (f a) ＝ η (a , refl)`. -To construct a contraction of `∥fiber f b∥_k` for each `b : B`, we have to show +To construct a contraction of `║fiber f b║ₖ` for each `b : B`, we have to show that ```text - (b : B) (u : ∥fiber f b∥_k) → c b ＝ u. + (b : B) (u : ║fiber f b║ₖ) → c b ＝ u. ``` Since the type `c b ＝ u` is `k`-truncated, this type is equivalent to the type diff --git a/src/foundation/multivariable-correspondences.lagda.md b/src/foundation/multivariable-correspondences.lagda.md index 6e422d49e7..9d753057aa 100644 --- a/src/foundation/multivariable-correspondences.lagda.md +++ b/src/foundation/multivariable-correspondences.lagda.md @@ -19,7 +19,7 @@ open import univalent-combinatorics.standard-finite-types ## Idea Consider a family of types `A` indexed by `Fin n`. An `n`-ary correspondence of -tuples `(x₁,...,x_n)` where `x_i : A_i` is a type family over +tuples `(x₁, …, xₙ)` where `x_i : A_i` is a type family over `(i : Fin n) → A i`. ## Definition diff --git a/src/foundation/singleton-subtypes.lagda.md b/src/foundation/singleton-subtypes.lagda.md index bfa09f5074..b624eca1cc 100644 --- a/src/foundation/singleton-subtypes.lagda.md +++ b/src/foundation/singleton-subtypes.lagda.md @@ -219,14 +219,14 @@ module _ **Proof:** Our goal is to show that the type ```text - Σ Y (λ y → ∥ Σ (Σ X (λ u → x ＝ u)) (λ v → f (inclusion v) ＝ y) ∥ ) + Σ Y (λ y → ║ Σ (Σ X (λ u → x ＝ u)) (λ v → f (inclusion v) ＝ y) ║ ) ``` Since the type `Σ X (λ u → x ＝ u)` is contractible, the above type is [equivalent](foundation-core.equivalences.md) to ```text - Σ Y (λ y → ∥ f x ＝ y ∥ ) + Σ Y (λ y → ║ f x ＝ y ║ ) ``` Note that the identity type `f x ＝ y` of a [set](foundation-core.sets.md) is a diff --git a/src/foundation/small-universes.lagda.md b/src/foundation/small-universes.lagda.md index 49a5bb6048..fda8cb43a0 100644 --- a/src/foundation/small-universes.lagda.md +++ b/src/foundation/small-universes.lagda.md @@ -17,8 +17,10 @@ open import foundation-core.small-types ## Idea -A universe `UU l1` is said to be small with respect to `UU l2` if `UU l1` is a -`UU l2`-small type and each `X : UU l1` is a `UU l2`-small type +A [universe](foundation.universe-levels.md) `𝒰` is said to be +{{#concept "small" Disambiguation="universe of types" Agda=is-small-universe}} +with respect to `𝒱` if `𝒰` is a `𝒱`-[small](foundation-core.small-types.md) type +and each `X : 𝒰` is a `𝒱`-small type. ```agda is-small-universe : diff --git a/src/foundation/truncation-equivalences.lagda.md b/src/foundation/truncation-equivalences.lagda.md index e32a7406dc..8d8ecf5786 100644 --- a/src/foundation/truncation-equivalences.lagda.md +++ b/src/foundation/truncation-equivalences.lagda.md @@ -300,11 +300,11 @@ We consider the following composition of maps ```text fiber f b = Σ A (λ a → f a = b) - → Σ A (λ a → ∥ f a ＝ b ∥) + → Σ A (λ a → ║ f a ＝ b ║) ≃ Σ A (λ a → | f a | = | b | - ≃ Σ A (λ a → ∥ f ∥ | a | = | b |) - → Σ ∥ A ∥ (λ t → ∥ f ∥ t = | b |) - = fiber ∥ f ∥ | b | + ≃ Σ A (λ a → ║ f ║ | a | = | b |) + → Σ ║ A ║ (λ t → ║ f ║ t = | b |) + = fiber ║ f ║ | b | ``` where the first and last maps are `k`-equivalences. diff --git a/src/graph-theory/polygons.lagda.md b/src/graph-theory/polygons.lagda.md index 2b21ec44ef..5224b39ed3 100644 --- a/src/graph-theory/polygons.lagda.md +++ b/src/graph-theory/polygons.lagda.md @@ -36,7 +36,7 @@ graph with vertices the underlying type of the [standard cyclic group](elementary-number-theory.standard-cyclic-groups.md) `ℤ-Mod k` and an edge from each `x ∈ ℤ-Mod k` to `x+1`. This defines for each `k ∈ ℕ` the type of all `k`-gons. The type of all `k`-gons is a concrete -presentation of the [dihedral group](group-theory.dihedral-groups.md) `D_k`. +presentation of the [dihedral group](group-theory.dihedral-groups.md) `Dₖ`. ## Definition diff --git a/src/group-theory/dihedral-groups.lagda.md b/src/group-theory/dihedral-groups.lagda.md index 526451b1ce..83fd4ee34a 100644 --- a/src/group-theory/dihedral-groups.lagda.md +++ b/src/group-theory/dihedral-groups.lagda.md @@ -20,8 +20,8 @@ open import group-theory.groups ## Idea -The dihedral group `D_k` is defined by the dihedral group construction applied -to the cyclic group `ℤ-Mod k`. +The dihedral group `Dₖ` is defined by the dihedral group construction applied to +the cyclic group `ℤ-Mod k`. ## Definition diff --git a/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md b/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md index 8a0dddce3b..364ee7abc8 100644 --- a/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md +++ b/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md @@ -17,6 +17,7 @@ open import elementary-number-theory.fermat-numbers open import elementary-number-theory.fibonacci-sequence open import elementary-number-theory.infinitude-of-primes open import elementary-number-theory.kolakoski-sequence +open import elementary-number-theory.multiset-coefficients open import elementary-number-theory.natural-numbers open import elementary-number-theory.pisano-periods @@ -43,6 +44,21 @@ A000002 : ℕ → ℕ A000002 = kolakoski ``` +### [A000004](https://oeis.org/A000004) The zero sequence + +```agda +A000004 : ℕ → ℕ +A000004 _ = zero-ℕ +``` + +### [A000007](https://oeis.org/A000007) The characteristic function for 0 + +```agda +A000007 : ℕ → ℕ +A000007 zero-ℕ = 1 +A000007 (succ-ℕ _) = 0 +``` + ### [A000010](https://oeis.org/A000010) Euler's totient function ```agda @@ -50,6 +66,20 @@ A000010 : ℕ → ℕ A000010 = eulers-totient-function-relatively-prime ``` +### [A000012](https://oeis.org/A000012) All 1's sequence + +```agda +A000012 : ℕ → ℕ +A000012 _ = 1 +``` + +### [A000027](https://oeis.org/A000027) The positive integers + +```agda +A000027 : ℕ → ℕ +A000027 = succ-ℕ +``` + ### [A000040](https://oeis.org/A000040) The prime numbers ```agda diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md index 7330b0cf07..054f1135dc 100644 --- a/src/set-theory.lagda.md +++ b/src/set-theory.lagda.md @@ -1,5 +1,44 @@ # Set theory +## Idea + +In univalent type theory, what we refer to formally as a _set_ is only in one +sense what is clasically understood to be a "set". Namely, we say a set is a +type whose [equality relation](foundation-core.identity-types.md) is a +[proposition](foundation-core.propositions.md). I.e., any two elements can be +equal in [at most one](foundation.subterminal-types.md) way. + +However, both historically {{#cite FBL73}} and in contemporary mathematics +{{#cite Kunen11}}, what is usually meant by set theory is the study of a +collection of related formal theories whose building blocks include a concept of +_sets_ and a propositionally valued _elementhood relation_, or _membership +relation_, `∈` on them. + +While this elementhood relation is not built into Martin–Löf type theory as a +fundamental construct, there is one important instance of it present in Agda — +namely, the [smallness](foundation-core.small-types.md) predicate: + +```text + is-small l A := Σ (X : UU l), (A ≃ X). +``` + +We can say that a type `A` _is an element of_ `UU l` if `A` is `UU l`-small in +this sense. Indeed, that `is-small l` is a predicate is equivalent to the +[univalence axiom](foundation-core.univalence.md). This highlights a second +connection between set theory and univalent type theory that is not directly +compatible with the preconception that "set theory is a study of set-level +mathematics". Namely, the universe of sets need not itself be a set-level +structure. In fact, with univalence it is a +[1-type](foundation-core.1-types.md). + +In this module, we consider ideas historically related to the study of set +theories both as foundations of set-level mathematics, but also as a study of +hierarchies in mathematics. This includes ideas such as +[cardinality](set-theory.cardinalities.md) and +[infinity](set-theory.infinite-sets.md), the +[cumulative hierarchy](set-theory.cumulative-hierarchy.md) as a model of set +theory, and [Russell's paradox](set-theory.russells-paradox.md). + ## Modules in the set theory namespace ```agda @@ -12,5 +51,10 @@ open import set-theory.cardinalities public open import set-theory.countable-sets public open import set-theory.cumulative-hierarchy public open import set-theory.infinite-sets public +open import set-theory.russells-paradox public open import set-theory.uncountable-sets public ``` + +## References + +{{#bibliography}} diff --git a/src/foundation/russells-paradox.lagda.md b/src/set-theory/russells-paradox.lagda.md similarity index 59% rename from src/foundation/russells-paradox.lagda.md rename to src/set-theory/russells-paradox.lagda.md index a778ee4a32..9ca07432a8 100644 --- a/src/foundation/russells-paradox.lagda.md +++ b/src/set-theory/russells-paradox.lagda.md @@ -3,7 +3,7 @@ ```agda {-# OPTIONS --lossy-unification #-} -module foundation.russells-paradox where +module set-theory.russells-paradox where ```
Imports @@ -37,14 +37,17 @@ open import trees.universal-multiset ## Idea -Russell's paradox arises when a set of all sets is assumed to exist. In +{{#concept "Russell's paradox" WD="Russell's paradox" WDID=Q33401 Agda=paradox-Russell}} +arises when a [set](foundation-core.sets.md) of all sets is assumed to exist. In Russell's paradox it is of no importance that the elementhood relation takes -values in propositions. In other words, Russell's paradox arises similarly if -there is a multiset of all multisets. We will construct Russell's paradox from -the assumption that a universe `U` is equivalent to a type `A : U`. We conclude +values in [propositions](foundation-core.propositions.md). In other words, +Russell's paradox arises similarly if there is a [multiset](trees.multisets.md) +of all multisets. We will construct Russell's paradox from the assumption that a +[universe](foundation.universe-levels.md) `𝒰` is +[equivalent](foundation-core.equivalences.md) to a type `A : 𝒰`. We conclude that there can be no universe that is contained in itself. Furthermore, using -replacement we show that for any type `A : U`, there is no surjective map -`A → U`. +[replacement](foundation.replacement.md) we show that for any type `A : 𝒰`, +there is no [surjective](foundation.surjective-maps.md) map `A → 𝒰`. ## Definition @@ -54,8 +57,8 @@ replacement we show that for any type `A : U`, there is no surjective map Russell : (l : Level) → 𝕍 (lsuc l) Russell l = comprehension-𝕍 - ( universal-multiset-𝕍 l) - ( λ X → X ∉-𝕍 X) + (universal-multiset-𝕍 l) + (λ X → X ∉-𝕍 X) ``` ## Properties @@ -63,37 +66,36 @@ Russell l = ### If a universe is small with respect to another universe, then Russells multiset is also small ```agda -is-small-Russell : - {l1 l2 : Level} → is-small-universe l2 l1 → is-small-𝕍 l2 (Russell l1) -is-small-Russell {l1} {l2} H = - is-small-comprehension-𝕍 l2 - { lsuc l1} - { universal-multiset-𝕍 l1} - { λ z → z ∉-𝕍 z} - ( is-small-universal-multiset-𝕍 l2 H) - ( λ X → is-small-∉-𝕍 l2 {l1} {X} {X} (K X) (K X)) +module _ + {l1 l2 : Level} (H : is-small-universe l2 l1) where - K = is-small-multiset-𝕍 (λ A → pr2 H A) - -resize-Russell : - {l1 l2 : Level} → is-small-universe l2 l1 → 𝕍 l2 -resize-Russell {l1} {l2} H = - resize-𝕍 (Russell l1) (is-small-Russell H) - -is-small-resize-Russell : - {l1 l2 : Level} (H : is-small-universe l2 l1) → - is-small-𝕍 (lsuc l1) (resize-Russell H) -is-small-resize-Russell {l1} {l2} H = - is-small-resize-𝕍 (Russell l1) (is-small-Russell H) - -equiv-Russell-in-Russell : - {l1 l2 : Level} (H : is-small-universe l2 l1) → - (Russell l1 ∈-𝕍 Russell l1) ≃ (resize-Russell H ∈-𝕍 resize-Russell H) -equiv-Russell-in-Russell H = - equiv-elementhood-resize-𝕍 (is-small-Russell H) (is-small-Russell H) + + is-small-Russell : is-small-𝕍 l2 (Russell l1) + is-small-Russell = + is-small-comprehension-𝕍 l2 + { lsuc l1} + { universal-multiset-𝕍 l1} + { λ z → z ∉-𝕍 z} + ( is-small-universal-multiset-𝕍 l2 H) + ( λ X → is-small-∉-𝕍 l2 (K X) (K X)) + where + K = is-small-multiset-𝕍 (pr2 H) + + resize-Russell : 𝕍 l2 + resize-Russell = resize-𝕍 (Russell l1) (is-small-Russell) + + is-small-resize-Russell : + is-small-𝕍 (lsuc l1) (resize-Russell) + is-small-resize-Russell = + is-small-resize-𝕍 (Russell l1) (is-small-Russell) + + equiv-Russell-in-Russell : + (Russell l1 ∈-𝕍 Russell l1) ≃ (resize-Russell ∈-𝕍 resize-Russell) + equiv-Russell-in-Russell = + equiv-elementhood-resize-𝕍 (is-small-Russell) (is-small-Russell) ``` -### Russell's paradox obtained from the assumption that `U` is `U`-small +### Russell's paradox obtained from the assumption that `𝒰` is `𝒰`-small ```agda paradox-Russell : {l : Level} → ¬ (is-small l (UU l)) @@ -147,13 +149,14 @@ paradox-Russell {l} H = ( associative-Σ ( 𝕍 l) ( λ t → t ∉-𝕍 t) - ( λ t → ( resize-𝕍 - ( pr1 t) - ( is-small-multiset-𝕍 is-small-lsuc (pr1 t))) ＝ - ( R)))))) + ( λ t → + ( resize-𝕍 + ( pr1 t) + ( is-small-multiset-𝕍 is-small-lsuc (pr1 t))) ＝ + ( R)))))) ``` -### There can be no surjective map `f : A → U` for any `A : U` +### There can be no surjective map `f : A → 𝒰` for any `A : 𝒰` ```agda no-surjection-onto-universe : @@ -164,3 +167,10 @@ no-surjection-onto-universe f H = ( is-small') ( is-locally-small-UU)) ``` + +## External links + +- [Russell's paradox](https://ncatlab.org/nlab/show/Russell%27s+paradox) at + $n$Lab +- [Russell's paradox](https://en.wikipedia.org/wiki/Russell%27s_paradox) at + Wikipedia diff --git a/src/trees/multisets.lagda.md b/src/trees/multisets.lagda.md index 57c1a96671..ed24b4339c 100644 --- a/src/trees/multisets.lagda.md +++ b/src/trees/multisets.lagda.md @@ -20,8 +20,9 @@ open import trees.w-types ## Idea -The type of **multisets** of universe level `l` is the W-type of the universal -family over the universe `UU l`. +The type of {{#concept "multisets" Agda=𝕍}} of +[universe level](foundation.universe-levels.md) `l` is the +[W-type](trees.w-types.md) of the universal family over the universe `UU l`. ## Definitions diff --git a/src/trees/small-multisets.lagda.md b/src/trees/small-multisets.lagda.md index fd3089d8d9..6a8bc2b79f 100644 --- a/src/trees/small-multisets.lagda.md +++ b/src/trees/small-multisets.lagda.md @@ -16,6 +16,7 @@ open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.propositions +open import foundation.raising-universe-levels open import foundation.small-types open import foundation.subtypes open import foundation.transport-along-identifications @@ -30,9 +31,11 @@ open import trees.w-types ## Idea -A multiset `X := tree-𝕎 A α` is said to be **small** with respect to a universe -`UU l` if its symbol `A` is a small type with respect to `UU l`, and if each -`α x` is a small multiset with respect to `UU l`. +A [multiset](trees.multisets.md) `X := tree-𝕎 A α` is said to be +{{#concept "small" Disambiguation="multiset" Agda=is-small-𝕍}} with respect to a +[universe](foundation.universe-levels.md) `UU l` if its symbol `A` is a +[small type](foundation-core.small-types.md) with respect to `UU l`, and if +recursively each `α x` is a small multiset with respect to `UU l`. ## Definition @@ -123,7 +126,7 @@ is-small-∉-𝕍 : is-small-∉-𝕍 l {l1} {X} {Y} H K = is-small-Π ( is-small-∈-𝕍 l {l1} {X} {Y} H K) - ( λ x → pair (raise-empty l) (compute-raise-empty l)) + ( λ x → Raise l empty) ``` ### The resizing of a small multiset is small diff --git a/src/trees/universal-multiset.lagda.md b/src/trees/universal-multiset.lagda.md index 274f1dfe83..954321d15a 100644 --- a/src/trees/universal-multiset.lagda.md +++ b/src/trees/universal-multiset.lagda.md @@ -26,8 +26,10 @@ open import trees.w-types ## Idea -The **universal multiset** of universe level `l` is the multiset of level -`lsuc l` built out of `𝕍 l` and resizings of the multisets it contains +The {{#concept "universal multiset" Agda=universal-multiset-𝕍}} of +[universe level](foundation.universe-levels.md) `l` is the +[multiset](trees.multisets.md) of level `lsuc l` built out of `𝕍 l` and +resizings of the multisets it contains. ## Definition diff --git a/src/univalent-combinatorics/presented-pi-finite-types.lagda.md b/src/univalent-combinatorics/presented-pi-finite-types.lagda.md index 2edfa3492b..207c97c608 100644 --- a/src/univalent-combinatorics/presented-pi-finite-types.lagda.md +++ b/src/univalent-combinatorics/presented-pi-finite-types.lagda.md @@ -14,9 +14,9 @@ module univalent-combinatorics.presented-pi-finite-types where ## Idea -A type `A` is said to be finitely `π_0`-presented if there is a standard pruned +A type `A` is said to be finitely `π₀`-presented if there is a standard pruned tree `T` of height 1 so that `A` has a presentation of cardinality `width T`, -and `A` is said to be finitely `π_{n+1}`-presented if there is a standard pruned +and `A` is said to be finitely `πₙ₊₁`-presented if there is a standard pruned tree `T` of height `n+2` and a map `f : Fin (width T) → A` so that -`η ∘ f : Fin (width T) → ∥A∥_0` is an equivalence, and for each +`η ∘ f : Fin (width T) → ║A║₀` is an equivalence, and for each `x : Fin (width T)` the type `Ω (A, f x)` is