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

@@ -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}}},

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
 

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

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

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

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
 

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

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

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

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 :

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.

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
 

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
 

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,13 +44,42 @@ 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
 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

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}}