From 12d328b3545c0802ff9c8f70622075f73e5f293f Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 6 Oct 2024 15:52:40 +0200
Subject: [PATCH 01/14] misc typesetting

---
 src/elementary-number-theory/falling-factorials.lagda.md  | 4 +++-
 src/foundation/connected-maps.lagda.md                    | 8 ++++----
 src/foundation/multivariable-correspondences.lagda.md     | 2 +-
 src/foundation/singleton-subtypes.lagda.md                | 4 ++--
 src/foundation/truncation-equivalences.lagda.md           | 8 ++++----
 src/graph-theory/polygons.lagda.md                        | 2 +-
 src/group-theory/dihedral-groups.lagda.md                 | 4 ++--
 .../presented-pi-finite-types.lagda.md                    | 6 +++---
 8 files changed, 20 insertions(+), 18 deletions(-)

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

From 39f96653d2f8ef842304f8a03c71e10e74617ed3 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 6 Oct 2024 15:53:34 +0200
Subject: [PATCH 02/14] some number sequences

---
 .../multiset-coefficients.lagda.md            | 20 ++++++++--
 .../oeis.lagda.md                             | 37 +++++++++++++++++++
 2 files changed, 53 insertions(+), 4 deletions(-)

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/online-encyclopedia-of-integer-sequences/oeis.lagda.md b/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
index 8a0dddce3b..4c4e3a82a5 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
@@ -133,3 +163,10 @@ A006369 = map-collatz-bijection
 A046859 : ℕ → ℕ
 A046859 n = ackermann n n
 ```
+
+### [A088218](https://oeis.org/A088218) The total number of leaves in all rooted ordered trees with n edges
+
+```agda
+A088218 : ℕ → ℕ
+A088218 n = multiset-coefficient n n
+```

From a58ec77ff0eb0dbdd269694604a77c2015b3f9c7 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 6 Oct 2024 15:54:02 +0200
Subject: [PATCH 03/14] links in some idea sections

---
 src/foundation/axiom-of-choice.lagda.md |  8 ++++----
 src/foundation/small-universes.lagda.md |  6 ++++--
 src/trees/small-multisets.lagda.md      | 11 +++++++----
 src/trees/universal-multiset.lagda.md   |  6 ++++--
 4 files changed, 19 insertions(+), 12 deletions(-)

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/small-universes.lagda.md b/src/foundation/small-universes.lagda.md
index 49a5bb6048..a184924c73 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-core.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/trees/small-multisets.lagda.md b/src/trees/small-multisets.lagda.md
index fd3089d8d9..aa39907094 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-core.universe-levels.md) `UU l` if its symbol `A` is a
+[small type](fondation-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..211055241a 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-core.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
 

From 842bc1344abbec4385882ead63ec88b983f8d72e Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 6 Oct 2024 15:54:31 +0200
Subject: [PATCH 04/14] idea section `set-theory`

---
 src/set-theory.lagda.md | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md
index 7330b0cf07..65bad56a84 100644
--- a/src/set-theory.lagda.md
+++ b/src/set-theory.lagda.md
@@ -1,5 +1,40 @@
 # 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](subterminal-types.md) way.
+
+However, both historicallly and in contemporary mathematics, what is commonly
+meant by set theory is also the study of a collection of related foundational
+theories whose basic notions include a _universe_ of _sets_ and a
+propositionally valued _elementhood relation_ on the universe of sets.
+
+While this elementhood relation is not built into type theory as a fundamental
+construct, there is a clear substitute for it — namely, the smallness predicate:
+
+```text
+  is-small l A := Σ (X : UU l), (A ≃ X).
+```
+
+We can say precisely 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
+which is incompatible with the assumption that "set theory must be a study of
+set-level mathematics".
+
+In this module, we assemble 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 for set
+theory, and [Russel's paradox](set-theory.russels-paradox.md).
+
 ## Modules in the set theory namespace
 
 ```agda

From 8ba19d5d59bfc6be1df93689b7a2e53c547e9bda Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 6 Oct 2024 15:54:49 +0200
Subject: [PATCH 05/14] move russels-paradox to set-theory

---
 src/foundation.lagda.md                       |  1 -
 src/set-theory.lagda.md                       |  1 +
 .../russells-paradox.lagda.md                 | 94 ++++++++++---------
 3 files changed, 53 insertions(+), 43 deletions(-)
 rename src/{foundation => set-theory}/russells-paradox.lagda.md (59%)

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/set-theory.lagda.md b/src/set-theory.lagda.md
index 65bad56a84..f326c20401 100644
--- a/src/set-theory.lagda.md
+++ b/src/set-theory.lagda.md
@@ -47,5 +47,6 @@ 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
 ```
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..0f1cd0d3f3 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
 ```
 
 <details><summary>Imports</summary>
@@ -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="Russel's paradox" WDID=Q33401 Agda=paradox-Russel}}
+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-leves.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
+
+- [Russel's paradox](https://ncatlab.org/nlab/show/Russell%27s+paradox) at
+  $n$Lab
+- [Russel's paradox](https://en.wikipedia.org/wiki/Russell%27s_paradox) at
+  Wikipedia

From dab7c8042f6ce58fcacfdad37bcf8fecd0e58413 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 6 Oct 2024 16:02:03 +0200
Subject: [PATCH 06/14] a word

---
 src/set-theory.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md
index f326c20401..481ee94669 100644
--- a/src/set-theory.lagda.md
+++ b/src/set-theory.lagda.md
@@ -23,8 +23,8 @@ construct, there is a clear substitute for it — namely, the smallness predicat
 We can say precisely 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
-which is incompatible with the assumption that "set theory must be a study of
+highlights a second connection between set theory and univalent type theory that
+is incompatible with the assumption that "set theory must be a study of
 set-level mathematics".
 
 In this module, we assemble ideas historically related to the study of set

From e94b1eb27225fc5c2ba2167dfab00d5b164b5cc0 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 6 Oct 2024 16:22:38 +0200
Subject: [PATCH 07/14] typo

---
 src/set-theory.lagda.md                  | 2 +-
 src/set-theory/russells-paradox.lagda.md | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md
index 481ee94669..ad92ad7df6 100644
--- a/src/set-theory.lagda.md
+++ b/src/set-theory.lagda.md
@@ -33,7 +33,7 @@ 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 for set
-theory, and [Russel's paradox](set-theory.russels-paradox.md).
+theory, and [Russell's paradox](set-theory.russells-paradox.md).
 
 ## Modules in the set theory namespace
 
diff --git a/src/set-theory/russells-paradox.lagda.md b/src/set-theory/russells-paradox.lagda.md
index 0f1cd0d3f3..11d502fb4b 100644
--- a/src/set-theory/russells-paradox.lagda.md
+++ b/src/set-theory/russells-paradox.lagda.md
@@ -37,7 +37,7 @@ open import trees.universal-multiset
 
 ## Idea
 
-{{#concept "Russell's paradox" WD="Russel's paradox" WDID=Q33401 Agda=paradox-Russel}}
+{{#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](foundation-core.propositions.md). In other words,
@@ -170,7 +170,7 @@ no-surjection-onto-universe f H =
 
 ## External links
 
-- [Russel's paradox](https://ncatlab.org/nlab/show/Russell%27s+paradox) at
+- [Russell's paradox](https://ncatlab.org/nlab/show/Russell%27s+paradox) at
   $n$Lab
-- [Russel's paradox](https://en.wikipedia.org/wiki/Russell%27s_paradox) at
+- [Russell's paradox](https://en.wikipedia.org/wiki/Russell%27s_paradox) at
   Wikipedia

From c08a79023a9ae8479881453ad1e5476430f2ab21 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 6 Oct 2024 18:09:30 +0200
Subject: [PATCH 08/14] fix links

---
 src/foundation/small-universes.lagda.md  | 2 +-
 src/set-theory.lagda.md                  | 2 +-
 src/set-theory/russells-paradox.lagda.md | 2 +-
 src/trees/multisets.lagda.md             | 5 +++--
 src/trees/small-multisets.lagda.md       | 4 ++--
 src/trees/universal-multiset.lagda.md    | 2 +-
 6 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/foundation/small-universes.lagda.md b/src/foundation/small-universes.lagda.md
index a184924c73..fda8cb43a0 100644
--- a/src/foundation/small-universes.lagda.md
+++ b/src/foundation/small-universes.lagda.md
@@ -17,7 +17,7 @@ open import foundation-core.small-types
 
 ## Idea
 
-A [universe](foundation-core.universe-levels.md) `𝒰` is said to be
+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.
diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md
index ad92ad7df6..e9e962e5c3 100644
--- a/src/set-theory.lagda.md
+++ b/src/set-theory.lagda.md
@@ -6,7 +6,7 @@ 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](subterminal-types.md) way.
+equal in [at most one](foundation.subterminal-types.md) way.
 
 However, both historicallly and in contemporary mathematics, what is commonly
 meant by set theory is also the study of a collection of related foundational
diff --git a/src/set-theory/russells-paradox.lagda.md b/src/set-theory/russells-paradox.lagda.md
index 11d502fb4b..9ca07432a8 100644
--- a/src/set-theory/russells-paradox.lagda.md
+++ b/src/set-theory/russells-paradox.lagda.md
@@ -43,7 +43,7 @@ Russell's paradox it is of no importance that the elementhood relation takes
 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-leves.md) `𝒰` is
+[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](foundation.replacement.md) we show that for any type `A : 𝒰`,
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 aa39907094..6a8bc2b79f 100644
--- a/src/trees/small-multisets.lagda.md
+++ b/src/trees/small-multisets.lagda.md
@@ -33,8 +33,8 @@ open import trees.w-types
 
 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-core.universe-levels.md) `UU l` if its symbol `A` is a
-[small type](fondation-core.small-types.md) with respect to `UU l`, and if
+[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
diff --git a/src/trees/universal-multiset.lagda.md b/src/trees/universal-multiset.lagda.md
index 211055241a..954321d15a 100644
--- a/src/trees/universal-multiset.lagda.md
+++ b/src/trees/universal-multiset.lagda.md
@@ -27,7 +27,7 @@ open import trees.w-types
 ## Idea
 
 The {{#concept "universal multiset" Agda=universal-multiset-𝕍}} of
-[universe level](foundation-core.universe-levels.md) `l` is the
+[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.
 

From 416e683a52e7841cf22c8956fddf7f0434a7d84b Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 6 Oct 2024 18:20:20 +0200
Subject: [PATCH 09/14] improve idea section

---
 src/set-theory.lagda.md | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md
index e9e962e5c3..55ba10109b 100644
--- a/src/set-theory.lagda.md
+++ b/src/set-theory.lagda.md
@@ -8,13 +8,14 @@ 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 historicallly and in contemporary mathematics, what is commonly
+However, both historically and in contemporary mathematics, what is commonly
 meant by set theory is also the study of a collection of related foundational
 theories whose basic notions include a _universe_ of _sets_ and a
 propositionally valued _elementhood relation_ on the universe of sets.
 
 While this elementhood relation is not built into type theory as a fundamental
-construct, there is a clear substitute for it — namely, the smallness predicate:
+construct, there is one important observable instance of it — namely, the
+smallness predicate:
 
 ```text
   is-small l A := Σ (X : UU l), (A ≃ X).
@@ -24,8 +25,8 @@ We can say precisely 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 incompatible with the assumption that "set theory must be a study of
-set-level mathematics".
+is incompatible with the preconception that "set theory is a study of set-level
+mathematics".
 
 In this module, we assemble ideas historically related to the study of set
 theories both as foundations of set-level mathematics, but also as a study of

From a3dd1293d0637d7a1888b584840febfc063daa4b Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sun, 6 Oct 2024 18:23:10 +0200
Subject: [PATCH 10/14] improve idea section

---
 src/set-theory.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md
index 55ba10109b..6c69a8ce5b 100644
--- a/src/set-theory.lagda.md
+++ b/src/set-theory.lagda.md
@@ -10,7 +10,7 @@ equal in [at most one](foundation.subterminal-types.md) way.
 
 However, both historically and in contemporary mathematics, what is commonly
 meant by set theory is also the study of a collection of related foundational
-theories whose basic notions include a _universe_ of _sets_ and a
+theories whose building blocks include a _universe_ of _sets_ and a
 propositionally valued _elementhood relation_ on the universe of sets.
 
 While this elementhood relation is not built into type theory as a fundamental

From 98a0f1c0979f0a7100349b4ac7b1a739978c6055 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 7 Oct 2024 13:31:38 +0200
Subject: [PATCH 11/14] some more wording adjustments

---
 src/set-theory.lagda.md | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/set-theory.lagda.md b/src/set-theory.lagda.md
index 6c69a8ce5b..12577cec27 100644
--- a/src/set-theory.lagda.md
+++ b/src/set-theory.lagda.md
@@ -14,18 +14,18 @@ theories whose building blocks include a _universe_ of _sets_ and a
 propositionally valued _elementhood relation_ on the universe of sets.
 
 While this elementhood relation is not built into type theory as a fundamental
-construct, there is one important observable instance of it — namely, the
-smallness predicate:
+construct, there is one important instance of it present — namely, the smallness
+predicate:
 
 ```text
   is-small l A := Σ (X : UU l), (A ≃ X).
 ```
 
-We can say precisely 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 incompatible with the preconception that "set theory is a study of set-level
+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".
 
 In this module, we assemble ideas historically related to the study of set
@@ -33,7 +33,7 @@ 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 for set
+[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

From 5f8c3a4342fbe2955806b2cc113ac01cb18d5776 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 7 Oct 2024 15:51:10 +0200
Subject: [PATCH 12/14] fixes peano arithmetic

---
 .../peano-arithmetic.lagda.md                       | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

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

From af65f9c27a2521731969d4d5f8f93f62ab36e315 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 7 Oct 2024 18:54:32 +0200
Subject: [PATCH 13/14] remove a sequence

---
 src/online-encyclopedia-of-integer-sequences/oeis.lagda.md | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md b/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
index 4c4e3a82a5..364ee7abc8 100644
--- a/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
+++ b/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
@@ -163,10 +163,3 @@ A006369 = map-collatz-bijection
 A046859 : ℕ → ℕ
 A046859 n = ackermann n n
 ```
-
-### [A088218](https://oeis.org/A088218) The total number of leaves in all rooted ordered trees with n edges
-
-```agda
-A088218 : ℕ → ℕ
-A088218 n = multiset-coefficient n n
-```

From baf30b3179bf50a1ade9b5bf500a11c0310a2935 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 9 Oct 2024 20:26:13 +0200
Subject: [PATCH 14/14] review

---
 references.bib          | 34 +++++++++++++++++++++++++++++-----
 src/set-theory.lagda.md | 27 +++++++++++++++++----------
 2 files changed, 46 insertions(+), 15 deletions(-)

diff --git a/references.bib b/references.bib
index 4c31aee2eb..42812639b5 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,
@@ -259,6 +259,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},
@@ -299,6 +312,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/set-theory.lagda.md b/src/set-theory.lagda.md
index 12577cec27..054f1135dc 100644
--- a/src/set-theory.lagda.md
+++ b/src/set-theory.lagda.md
@@ -8,27 +8,30 @@ 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 and in contemporary mathematics, what is commonly
-meant by set theory is also the study of a collection of related foundational
-theories whose building blocks include a _universe_ of _sets_ and a
-propositionally valued _elementhood relation_ on the universe of sets.
+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 type theory as a fundamental
-construct, there is one important instance of it present — namely, the smallness
-predicate:
+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
+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".
+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 assemble ideas historically related to the study of set
+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
@@ -51,3 +54,7 @@ open import set-theory.infinite-sets public
 open import set-theory.russells-paradox public
 open import set-theory.uncountable-sets public
 ```
+
+## References
+
+{{#bibliography}}