From bf10991201482c399640e714a73068234d23dcc1 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 16 Oct 2024 16:43:50 +0200
Subject: [PATCH 1/4] a bunch of links in elementary number theory

---
 .../absolute-value-integers.lagda.md          |  4 +-
 .../ackermann-function.lagda.md               |  5 +-
 .../binomial-coefficients.lagda.md            | 21 ++++-
 .../catalan-numbers.lagda.md                  | 55 +++++++++++-
 .../cofibonacci.lagda.md                      | 13 ++-
 .../distance-natural-numbers.lagda.md         |  8 +-
 .../eulers-totient-function.lagda.md          | 10 ++-
 .../factorials.lagda.md                       | 11 +++
 .../fermat-numbers.lagda.md                   |  9 +-
 .../fibonacci-sequence.lagda.md               | 83 ++++++++++++-------
 ...fundamental-theorem-of-arithmetic.lagda.md | 37 ++++++---
 .../goldbach-conjecture.lagda.md              | 24 ++++++
 .../hardy-ramanujan-number.lagda.md           |  2 +-
 .../infinitude-of-primes.lagda.md             | 15 ++--
 .../integers.lagda.md                         |  4 +-
 .../jacobi-symbol.lagda.md                    | 14 +++-
 .../kolakoski-sequence.lagda.md               |  7 +-
 .../legendre-symbol.lagda.md                  |  4 +-
 .../natural-numbers.lagda.md                  |  7 +-
 .../peano-arithmetic.lagda.md                 |  2 +-
 .../taxicab-numbers.lagda.md                  |  2 +-
 .../telephone-numbers.lagda.md                |  9 +-
 .../acyclic-undirected-graphs.lagda.md        |  2 +-
 .../circuits-undirected-graphs.lagda.md       |  2 +-
 .../closed-walks-undirected-graphs.lagda.md   |  2 +-
 .../complete-bipartite-graphs.lagda.md        |  2 +-
 .../complete-multipartite-graphs.lagda.md     |  2 +-
 .../complete-undirected-graphs.lagda.md       |  2 +-
 .../connected-undirected-graphs.lagda.md      |  2 +-
 .../cycles-undirected-graphs.lagda.md         |  2 +-
 ...tructures-on-standard-finite-sets.lagda.md |  2 +-
 src/graph-theory/directed-graphs.lagda.md     |  2 +-
 .../edge-coloured-undirected-graphs.lagda.md  |  2 +-
 .../enriched-undirected-graphs.lagda.md       |  2 +-
 .../equivalences-directed-graphs.lagda.md     |  2 +-
 ...lences-enriched-undirected-graphs.lagda.md |  2 +-
 .../equivalences-undirected-graphs.lagda.md   |  2 +-
 src/graph-theory/hypergraphs.lagda.md         |  2 +-
 .../large-reflexive-graphs.lagda.md           |  2 +-
 src/graph-theory/matchings.lagda.md           |  2 +-
 ...re-equivalences-undirected-graphs.lagda.md |  2 +-
 .../neighbors-undirected-graphs.lagda.md      |  2 +-
 .../orientations-undirected-graphs.lagda.md   |  2 +-
 .../paths-undirected-graphs.lagda.md          |  2 +-
 src/graph-theory/polygons.lagda.md            |  2 +-
 src/graph-theory/reflexive-graphs.lagda.md    |  2 +-
 .../regular-undirected-graphs.lagda.md        |  2 +-
 .../simple-undirected-graphs.lagda.md         |  2 +-
 .../trails-directed-graphs.lagda.md           |  2 +-
 .../trails-undirected-graphs.lagda.md         |  2 +-
 ...tructures-on-standard-finite-sets.lagda.md |  2 +-
 src/graph-theory/undirected-graphs.lagda.md   |  2 +-
 src/graph-theory/vertex-covers.lagda.md       |  2 +-
 .../walks-directed-graphs.lagda.md            |  2 +-
 .../walks-undirected-graphs.lagda.md          |  2 +-
 .../abelianization-groups.lagda.md            |  2 +-
 .../commutator-subgroups.lagda.md             |  2 +-
 .../commutators-of-elements-groups.lagda.md   |  2 +-
 ...zer-groups-concrete-group-actions.lagda.md |  2 +-
 src/group-theory/stabilizer-groups.lagda.md   |  2 +-
 .../oeis.lagda.md                             | 17 ++++
 .../binomial-types.lagda.md                   |  3 +-
 62 files changed, 322 insertions(+), 120 deletions(-)

diff --git a/src/elementary-number-theory/absolute-value-integers.lagda.md b/src/elementary-number-theory/absolute-value-integers.lagda.md
index 63a02a8915..59455c73a5 100644
--- a/src/elementary-number-theory/absolute-value-integers.lagda.md
+++ b/src/elementary-number-theory/absolute-value-integers.lagda.md
@@ -28,8 +28,8 @@ open import foundation.unit-type
 
 ## Idea
 
-The absolute value of an integer is the natural number with the same distance
-from `0`.
+The {{#concept "absolute value" Disambiguation="of an integer" Agda=abs-ℤ}} of
+an integer is the natural number with the same distance from `0`.
 
 ## Definition
 
diff --git a/src/elementary-number-theory/ackermann-function.lagda.md b/src/elementary-number-theory/ackermann-function.lagda.md
index 23136504b7..be5add2d11 100644
--- a/src/elementary-number-theory/ackermann-function.lagda.md
+++ b/src/elementary-number-theory/ackermann-function.lagda.md
@@ -14,8 +14,9 @@ open import elementary-number-theory.natural-numbers
 
 ## Idea
 
-The Ackermann function is a fast growing binary operation on the natural
-numbers.
+The
+{{#concept "Ackermann function" WD="Ackermann function" WDID=Q341835 Agda=ackermann}}
+is a fast growing binary operation on the natural numbers.
 
 ## Definition
 
diff --git a/src/elementary-number-theory/binomial-coefficients.lagda.md b/src/elementary-number-theory/binomial-coefficients.lagda.md
index 47b9960243..93e627dd0f 100644
--- a/src/elementary-number-theory/binomial-coefficients.lagda.md
+++ b/src/elementary-number-theory/binomial-coefficients.lagda.md
@@ -20,8 +20,12 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-The binomial coefficient `(n choose k)` measures how many decidable subsets of
-`Fin n` there are of size `k`.
+The
+{{#concept "binomial coefficient" WD="binomial coefficient" WDID=Q209875 Agda=binomial-coefficient-ℕ}}
+`(n choose k)` measures
+[how many decidable subsets](univalent-combinatorics.counting-decidable-subtypes.md)
+of size `k` there are of a
+[finite type](univalent-combinatorics.finite-types.md) of size `n`.
 
 ## Definition
 
@@ -68,3 +72,16 @@ is-one-on-diagonal-binomial-coefficient-ℕ (succ-ℕ n) =
     ( is-one-on-diagonal-binomial-coefficient-ℕ n)
     ( is-zero-binomial-coefficient-ℕ n (succ-ℕ n) (succ-le-ℕ n))
 ```
+
+## See also
+
+- [Binomial types](univalent-combinatorics.binomial-types.md)
+
+## External links
+
+- [Binomial coefficients](https://www.britannica.com/science/binomial-coefficient)
+  at Britannica
+- [Binomial coefficient](https://en.wikipedia.org/wiki/Binomial_coefficient) at
+  Wikipedia
+- [Binomial Coefficient](https://mathworld.wolfram.com/BinomialCoefficient.html)
+  at Wolfram MathWorld
diff --git a/src/elementary-number-theory/catalan-numbers.lagda.md b/src/elementary-number-theory/catalan-numbers.lagda.md
index 5abda815f6..ccec4a8716 100644
--- a/src/elementary-number-theory/catalan-numbers.lagda.md
+++ b/src/elementary-number-theory/catalan-numbers.lagda.md
@@ -22,15 +22,46 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-The Catalan numbers are a sequence of natural numbers that occur in several
-combinatorics problems.
+The
+{{#concept "Catalan numbers" WD="Catalan number" WDID=Q270513 OEIS=A000108 Agda=catalan-numbers}}
+$C_n$ is a [sequence](foundation.sequences.md) of
+[natural numbers](elementary-number-theory.natural-numbers.md) that occur in
+several combinatorics problems. The sequence starts
+
+```text
+  n   0   1   2   3   4   5   6
+  Cₙ  1   1   2   5  14  42 132 ⋯
+```
+
+The Catalan numbers may be defined by any of the formulas
+
+1. $C_{n + 1} = \sum_{k = 0}^n C_k C_{n-k}$, with $C_0 = 1$,
+2. $C_n = {2n \choose n} - {2n \choose n + 1}$,
+3. $C_{n+1} = \frac{2(2n+1)}{n+2}C_n$, with $C_0 = 1$,
+4. $C_{n} = \frac{1}{n+1}{2n \choose n}$,
+5. $C_{n} = \frac{(2n)!}{(n+1)!n!}$.
+
+Where $n \choose k$ are
+[binomial coefficients](elementary-number-theory.binomial-coefficients.md) and
+$n!$ is the [factorial function](elementary-number-theory.factorials.md).
 
 ## Definitions
 
+### Inductive sum formula for the Catalan numbers
+
+The Catalan numbers may be defined to be the sequence satisfying $C_0 = 1$ and
+the recurrence relation
+
+$$
+C_{n + 1} = \sum_{k = 0}^n C_k C_{n-k}.
+$$
+
 ```agda
 catalan-numbers : ℕ → ℕ
 catalan-numbers =
-  strong-ind-ℕ (λ _ → ℕ) (succ-ℕ zero-ℕ)
+  strong-ind-ℕ
+    ( λ _ → ℕ)
+    ( 1)
     ( λ k C →
       sum-Fin-ℕ k
         ( λ i →
@@ -45,10 +76,28 @@ catalan-numbers =
                     ( nat-Fin k i)
                     ( k)
                     ( strict-upper-bound-nat-Fin k i))))))
+```
+
+### Binomial difference formula for the Catalan numbers
+
+The Catalan numbers may be computed as a difference of consecutive binomial
+coefficients
+
+$$
+C_n = {2n \choose n} - {2n \choose n + 1}.
+$$
 
+```agda
 catalan-numbers-binomial : ℕ → ℕ
 catalan-numbers-binomial n =
   dist-ℕ
     ( binomial-coefficient-ℕ (2 *ℕ n) n)
     ( binomial-coefficient-ℕ (2 *ℕ n) (succ-ℕ n))
 ```
+
+## External links
+
+- [Catalan number](https://en.wikipedia.org/wiki/Catalan_number) at Wikipedia
+- [Catalan Number](https://mathworld.wolfram.com/CatalanNumber.html) at Wolfram
+  MathWorld
+- [A000108](https://oeis.org/A000108) in the OEIS
diff --git a/src/elementary-number-theory/cofibonacci.lagda.md b/src/elementary-number-theory/cofibonacci.lagda.md
index a5c3b562c0..e2a6f001ba 100644
--- a/src/elementary-number-theory/cofibonacci.lagda.md
+++ b/src/elementary-number-theory/cofibonacci.lagda.md
@@ -30,13 +30,20 @@ open import foundation.universe-levels
 
 ## Idea
 
-The [**cofibonacci sequence**][1] is the unique function G : ℕ → ℕ satisfying
-the property that
+The {{#concept "cofibonacci sequence" Agda=cofibonacci}} is the unique function
+`G : ℕ → ℕ` satisfying the property that
 
 ```text
   div-ℕ (G m) n ↔ div-ℕ m (Fibonacci-ℕ n).
 ```
 
+The sequence starts
+
+```text
+  n   0   1   2   3   4   5   6   7   8   9  10  11  12  13
+  Gₙ  1   3   4   6   5  12   8   6  12  15  10  12   7  24  ⋯
+```
+
 ## Definitions
 
 ### The predicate of being a multiple of the `m`-th cofibonacci number
@@ -141,4 +148,4 @@ is-left-adjoint-cofibonacci m n = {!!}
 
 ## External links
 
-[1]: https://oeis.org/A001177
+- [A001177](https://oeis.org/A001177) in the OEIS
diff --git a/src/elementary-number-theory/distance-natural-numbers.lagda.md b/src/elementary-number-theory/distance-natural-numbers.lagda.md
index 0426593e35..1e04905a6a 100644
--- a/src/elementary-number-theory/distance-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/distance-natural-numbers.lagda.md
@@ -28,9 +28,11 @@ open import foundation.universe-levels
 
 ## Idea
 
-The distance function between natural numbers measures how far two natural
-numbers are apart. In the agda-unimath library we often prefer to work with
-`dist-ℕ` over the partially defined subtraction operation.
+The
+{{#concept "distance function" Disambiguation="between natural numbers" Agda=dist-ℕ}}
+between [natural numbers](elementary-number-theory.natural-numbers.md) measures
+how far two natural numbers are apart. In the agda-unimath library we often
+prefer to work with `dist-ℕ` over the partially defined subtraction operation.
 
 ## Definition
 
diff --git a/src/elementary-number-theory/eulers-totient-function.lagda.md b/src/elementary-number-theory/eulers-totient-function.lagda.md
index a538eb57dd..67c4aa43d1 100644
--- a/src/elementary-number-theory/eulers-totient-function.lagda.md
+++ b/src/elementary-number-theory/eulers-totient-function.lagda.md
@@ -19,7 +19,8 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-**Euler's totient function** `φ : ℕ → ℕ` is the function that maps a
+{{#concept "Euler's totient function" WD="Euler's totient function" WDID=Q190026 Agda=eulers-totient-function-relatively-prime}}
+`φ : ℕ → ℕ` is the function that maps a
 [natural number](elementary-number-theory.natural-numbers.md) `n` to the number
 of
 [multiplicative units modulo `n`](elementary-number-theory.multiplicative-units-standard-cyclic-rings.md).
@@ -57,3 +58,10 @@ eulers-totient-function-relatively-prime n =
 ### Table of files related to cyclic types, groups, and rings
 
 {{#include tables/cyclic-types.md}}
+
+## External links
+
+- [Euler's totient function](https://en.wikipedia.org/wiki/Euler%27s_totient_function)
+  at Wikipedia
+- [Totient Function](https://mathworld.wolfram.com/TotientFunction.html) at
+  Wolfram MathWorld
diff --git a/src/elementary-number-theory/factorials.lagda.md b/src/elementary-number-theory/factorials.lagda.md
index 7affe83e4f..05851e426e 100644
--- a/src/elementary-number-theory/factorials.lagda.md
+++ b/src/elementary-number-theory/factorials.lagda.md
@@ -21,6 +21,12 @@ open import foundation.identity-types
 
 </details>
 
+## Idea
+
+The {{#concept "factorial" WD="factorial" WDID=Q120976 Agda=factorial-ℕ}} `n!`
+of a number `n`, counts the number of ways to linearly order `n` distinct
+objects.
+
 ## Definition
 
 ```agda
@@ -66,3 +72,8 @@ leq-factorial-ℕ (succ-ℕ n) =
     ( succ-ℕ n)
     ( is-nonzero-factorial-ℕ n)
 ```
+
+## External links
+
+- [Factorial](https://en.wikipedia.org/wiki/Factorial) at Wikipedia
+- [A000142](https://oeis.org/A000142) in the OEIS
diff --git a/src/elementary-number-theory/fermat-numbers.lagda.md b/src/elementary-number-theory/fermat-numbers.lagda.md
index 5e334c8a57..25be74d35c 100644
--- a/src/elementary-number-theory/fermat-numbers.lagda.md
+++ b/src/elementary-number-theory/fermat-numbers.lagda.md
@@ -20,8 +20,8 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-{{#concept "Fermat numbers"}} are numbers of the form $F_n := 2^{2^n}+1$. The
-first five Fermat numbers are
+{{#concept "Fermat numbers" WD="Fermat number" WDID=Q207264 Agda=fermat-number-ℕ}}
+are numbers of the form $F_n := 2^{2^n}+1$. The first five Fermat numbers are
 
 ```text
   3, 5, 17, 257, and 65537.
@@ -72,3 +72,8 @@ recursive-fermat-number-ℕ =
           ( λ i → f (nat-Fin (succ-ℕ n) i) (upper-bound-nat-Fin n i)))
         ( 2))
 ```
+
+## External link
+
+- [Fermat number](https://en.wikipedia.org/wiki/Fermat_number) at Wikipedia
+- [A000215](https://oeis.org/A000215) in the OEIS
diff --git a/src/elementary-number-theory/fibonacci-sequence.lagda.md b/src/elementary-number-theory/fibonacci-sequence.lagda.md
index 634cc34706..89af95e039 100644
--- a/src/elementary-number-theory/fibonacci-sequence.lagda.md
+++ b/src/elementary-number-theory/fibonacci-sequence.lagda.md
@@ -22,6 +22,27 @@ open import foundation.transport-along-identifications
 
 </details>
 
+## Idea
+
+The
+{{#concept "Fibonacci sequence" WD="Fibonacci sequence" WDID=Q23835349 Agda=Fibonacci-ℕ}}
+is a recursively defined [sequence](foundation.sequences.md) of
+[natural numbers](elementary-number-theory.natural-numbers.md) given by the
+equations
+
+```text
+  Fₙ₊₂ = Fₙ₊₁ + Fₙ,   where F₀ = 0 and F₁ = 1
+```
+
+A number in this sequence is called a
+{{#concept "Fibonacci number" WD="Fibonacci number" WDID=Q47577}}. The first few
+Fibonacci numbers are
+
+```text
+  n    0   1   2   3   4   5   6   7   8   9
+  Fₙ   0   1   1   2   3   5   8  13  21  34
+```
+
 ## Definitions
 
 ### The standard definition using pattern matching
@@ -93,34 +114,34 @@ Fibonacci-add-ℕ m zero-ℕ =
     ( inv (right-zero-law-mul-ℕ (Fibonacci-ℕ m)))
 Fibonacci-add-ℕ m (succ-ℕ n) =
   ( ap Fibonacci-ℕ (inv (left-successor-law-add-ℕ m (succ-ℕ n)))) ∙
-  ( ( Fibonacci-add-ℕ (succ-ℕ m) n) ∙
-    ( ( ap
-        ( _+ℕ ((Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ n)))
-        ( right-distributive-mul-add-ℕ
-          ( Fibonacci-ℕ (succ-ℕ m))
-          ( Fibonacci-ℕ m)
-          ( Fibonacci-ℕ (succ-ℕ n)))) ∙
-      ( ( associative-add-ℕ
-          ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
-          ( (Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
-          ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ n))) ∙
-        ( ( ap
-            ( ((Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ (succ-ℕ n))) +ℕ_)
-            ( commutative-add-ℕ
-              ( (Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
-              ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ n)))) ∙
-          ( ( inv
-              ( associative-add-ℕ
-                ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
-                ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ n))
-                ( (Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ (succ-ℕ n))))) ∙
-            ( ap
-              ( _+ℕ ((Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ (succ-ℕ n))))
-              ( inv
-                ( left-distributive-mul-add-ℕ
-                  ( Fibonacci-ℕ (succ-ℕ m))
-                  ( Fibonacci-ℕ (succ-ℕ n))
-                  ( Fibonacci-ℕ n)))))))))
+  ( Fibonacci-add-ℕ (succ-ℕ m) n) ∙
+  ( ap
+    ( _+ℕ ((Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ n)))
+    ( right-distributive-mul-add-ℕ
+      ( Fibonacci-ℕ (succ-ℕ m))
+      ( Fibonacci-ℕ m)
+      ( Fibonacci-ℕ (succ-ℕ n)))) ∙
+  ( associative-add-ℕ
+    ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
+    ( (Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
+    ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ n))) ∙
+  ( ap
+    ( ((Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ (succ-ℕ n))) +ℕ_)
+    ( commutative-add-ℕ
+      ( (Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
+      ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ n)))) ∙
+  ( inv
+    ( associative-add-ℕ
+      ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ (succ-ℕ n)))
+      ( (Fibonacci-ℕ (succ-ℕ m)) *ℕ (Fibonacci-ℕ n))
+      ( (Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ (succ-ℕ n))))) ∙
+  ( ap
+    ( _+ℕ ((Fibonacci-ℕ m) *ℕ (Fibonacci-ℕ (succ-ℕ n))))
+    ( inv
+      ( left-distributive-mul-add-ℕ
+        ( Fibonacci-ℕ (succ-ℕ m))
+        ( Fibonacci-ℕ (succ-ℕ n))
+        ( Fibonacci-ℕ n))))
 ```
 
 ### Consecutive Fibonacci numbers are relatively prime
@@ -204,3 +225,9 @@ preserves-div-Fibonacci-ℕ :
 preserves-div-Fibonacci-ℕ m n H =
   div-Fibonacci-div-ℕ (Fibonacci-ℕ m) m n H (refl-div-ℕ (Fibonacci-ℕ m))
 ```
+
+## External links
+
+- [Fibonacci sequence](https://en.wikipedia.org/wiki/Fibonacci_sequence) at
+  Wikipedia
+- [A000045](https://oeis.org/A000045) in the OEIS
diff --git a/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md b/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md
index 5f3f725db7..14e7d534e3 100644
--- a/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md
+++ b/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md
@@ -53,31 +53,37 @@ open import lists.sorted-lists
 
 ## Idea
 
-The **fundamental theorem of arithmetic** asserts that every nonzero natural
-number can be written as a product of primes, and this product is unique up to
-the order of the factors.
+The
+{{#concept "fundamental theorem of arithmetic" WD="fundamental theorem of arithmetic" WDID=Q670235 Agda=fundamental-theorem-arithmetic-list-ℕ}}
+asserts that every
+[nonzero](elementary-number-theory.nonzero-natural-numbers.md)
+[natural number](elementary-number-theory.natural-numbers.md) can be written as
+a [product](elementary-number-theory.products-of-natural-numbers.md) of
+[primes](elementary-number-theory.prime-numbers.md), and this product is
+[unique](foundation-core.contractible-types.md) up to the order of the factors.
 
 The uniqueness of the prime factorization of a natural number can be expressed
 in several ways:
 
-- We can find a unique list of primes `p₁ ≤ p₂ ≤ ⋯ ≤ pᵢ` of which the product is
-  equal to `n`
-- The type of finite sets `X` equipped with functions `p : X → Σ ℕ is-prime-ℕ`
-  and `m : X → positive-ℕ` such that the product of `pₓᵐ⁽ˣ⁾` is equal to `n` is
-  contractible.
+- We can find a unique [list](lists.lists.md) of primes `p₁ ≤ p₂ ≤ ⋯ ≤ pᵢ` of
+  which the product is equal to `n`
+- The type of [finite sets](univalent-combinatorics.finite-types.md) `X`
+  [equipped](foundation.structure.md) with functions `p : X → Σ ℕ is-prime-ℕ`
+  and `m : X → positive-ℕ` such that the product of `pₓᵐ⁽ˣ⁾` is
+  [equal](foundation-core.identity-types.md) to `n` is contractible.
 
-Note that the univalence axiom is neccessary to prove the second uniqueness
-property of prime factorizations.
+Note that the [univalence axiom](foundation-core.univalence.md) is neccessary to
+prove the second uniqueness property of prime factorizations.
 
 ## Definitions
 
 ### Prime decomposition of a natural number with lists
 
-A list of natural numbers is a prime decomposition of a natural number `n` if :
+A list of natural numbers is a prime decomposition of a natural number `n` if:
 
-- The list is sorted
+- The list is sorted.
 - Every element of the list is prime.
-- The product of the element of the list is equal to `n`
+- The product of the element of the list is equal to `n`.
 
 ```agda
 is-prime-list-ℕ :
@@ -1075,3 +1081,8 @@ pr1 (prime-decomposition-list-sort-concatenation-ℕ x y H I p q Dp Dq) =
 pr2 (prime-decomposition-list-sort-concatenation-ℕ x y H I p q Dp Dq) =
   is-prime-decomposition-list-sort-concatenation-ℕ x y H I p q Dp Dq
 ```
+
+## External links
+
+- [Fundamental theorem of arithmetic](https://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmetic)
+  at Wikipedia
diff --git a/src/elementary-number-theory/goldbach-conjecture.lagda.md b/src/elementary-number-theory/goldbach-conjecture.lagda.md
index eef772ea6c..ab096dfab1 100644
--- a/src/elementary-number-theory/goldbach-conjecture.lagda.md
+++ b/src/elementary-number-theory/goldbach-conjecture.lagda.md
@@ -21,6 +21,21 @@ open import foundation.universe-levels
 
 </details>
 
+## Idea
+
+The
+{{#concept "Goldbach conjecture" WD="Goldbach's conjecture" WDID=Q485520 Agda=Goldbach-conjecture}}
+states that every even
+[natural number](elementary-number-theory.natural-numbers.md) `n`
+[greater than](elementary-number-theory.strict-inequality-natural-numbers.md)
+two is [equal](foundation-core.identity-types.md) to a
+[sum](elementary-number-theory.addition-natural-numbers.md) of two
+[primes](elementary-number-theory.prime-numbers.md)
+
+```text
+  n = p + q.
+```
+
 ## Conjecture
 
 ```agda
@@ -29,3 +44,12 @@ Goldbach-conjecture =
   ( n : ℕ) → (le-ℕ 2 n) → (is-even-ℕ n) →
     Σ ℕ (λ p → (is-prime-ℕ p) × (Σ ℕ (λ q → (is-prime-ℕ q) × (p +ℕ q ＝ n))))
 ```
+
+## External links
+
+- [Goldbach conjecture](https://www.britannica.com/science/Goldbach-conjecture)
+  at Britannica
+- [Goldbach's conjecture](https://en.wikipedia.org/wiki/Goldbach%27s_conjecture)
+  at Wikipedia
+- [Goldbach Conjecture](https://mathworld.wolfram.com/GoldbachConjecture.html)
+  at Wolfram MathWorld
diff --git a/src/elementary-number-theory/hardy-ramanujan-number.lagda.md b/src/elementary-number-theory/hardy-ramanujan-number.lagda.md
index e12c9f0e09..9ecffa68bf 100644
--- a/src/elementary-number-theory/hardy-ramanujan-number.lagda.md
+++ b/src/elementary-number-theory/hardy-ramanujan-number.lagda.md
@@ -20,7 +20,7 @@ open import foundation.unit-type
 ## Idea
 
 The
-{{#concept "Hardy-Ramanujan number" Agda=Hardy-Ramanujan-ℕ WD="1729" WDID=Q825176}}
+{{#concept "Hardy-Ramanujan number" Agda=Hardy-Ramanujan-ℕ WD="1729" WDID=Q825176 Agda=Hardy-Ramanujan-ℕ}}
 is the number `1729`. This number is the second
 [taxicab number](elementary-number-theory.taxicab-numbers.md), i.e., it is the
 least natural number that can be written as a sum of cubes of positive natural
diff --git a/src/elementary-number-theory/infinitude-of-primes.lagda.md b/src/elementary-number-theory/infinitude-of-primes.lagda.md
index e106f39df4..e5c6ff0fa2 100644
--- a/src/elementary-number-theory/infinitude-of-primes.lagda.md
+++ b/src/elementary-number-theory/infinitude-of-primes.lagda.md
@@ -35,14 +35,19 @@ open import foundation.universe-levels
 
 ## Idea
 
-We show, using the sieve of Eratosthenes and the well-ordering principle of `ℕ`,
-that there are infinitely many primes. Consequently we obtain the function that
-returns for each `n` the `n`-th prime, and we obtain the function that counts
-the number of primes below a number `n`.
+We show, using the
+[sieve of Eratosthenes](elementary-number-theory.sieve-of-eratosthenes.md) and
+the
+[well-ordering principle of `ℕ`](elementary-number-theory.well-ordering-principle-natural-numbers.md),
+that there are infinitely many
+[primes](elementary-number-theory.prime-numbers.md). Consequently we obtain the
+function that returns for each `n` the `n`-th prime, and we obtain the function
+that counts the number of primes below a number `n`.
 
 ## Definition
 
-We begin by stating the infinitude of primes in type theory.
+We begin by stating the
+{{#concept "infinitude of primes" Agda=Infinitude-Of-Primes-ℕ}} in type theory.
 
 ```agda
 Infinitude-Of-Primes-ℕ : UU lzero
diff --git a/src/elementary-number-theory/integers.lagda.md b/src/elementary-number-theory/integers.lagda.md
index bc56a2ad9c..2c1ea175d6 100644
--- a/src/elementary-number-theory/integers.lagda.md
+++ b/src/elementary-number-theory/integers.lagda.md
@@ -37,7 +37,9 @@ open import structured-types.types-equipped-with-endomorphisms
 
 ## Idea
 
-The type of integers is an extension of the type of natural numbers including
+The type of {{#concept "integers" WD="integer" WDID=Q12503 Agda=ℤ}} is an
+extension of the type of
+[natural numbers](elementary-number-theory.natural-numbers.md) including
 negative whole numbers.
 
 ## Definitions
diff --git a/src/elementary-number-theory/jacobi-symbol.lagda.md b/src/elementary-number-theory/jacobi-symbol.lagda.md
index 8750c2e32c..b7c291a319 100644
--- a/src/elementary-number-theory/jacobi-symbol.lagda.md
+++ b/src/elementary-number-theory/jacobi-symbol.lagda.md
@@ -24,16 +24,22 @@ open import lists.lists
 
 ## Idea
 
-The **Jacobi symbol** is a function which encodes information about the
+The
+{{#concept "Jacobi symbol" WD="Jacobi symbol" WDID=Q241015 Agda=jacobi-symbol}}
+is a function which encodes information about the
 [squareness](elementary-number-theory.squares-modular-arithmetic.md) of an
 [integer](elementary-number-theory.integers.md) within certain
 [rings of integers modulo `p`](elementary-number-theory.modular-arithmetic.md),
 for [prime](elementary-number-theory.prime-numbers.md) `p`. Specifically,
 `jacobi-symbol(a,n)` for an integer `a : ℤ` and natural number `n : ℕ` is the
 product of the [legendre symbols](elementary-number-theory.legendre-symbol.md)
-`legendre-symbol(p₁,a),legendre-symbol(p₂,a),...,legendre-symbol(pₖ,a)`, where
-`p₁,...,pₖ` are the prime factors of `n`, not necessarily distinct (i.e. it is
-possible that `pᵢ = pⱼ`).
+
+```text
+  legendre-symbol(p₁,a) · legendre-symbol(p₂,a) · … · legendre-symbol(pₖ,a),
+```
+
+where `p₁, …, pₖ` are the prime factors of `n`, not necessarily distinct (i.e.
+it is possible that `pᵢ = pⱼ`).
 
 ## Definition
 
diff --git a/src/elementary-number-theory/kolakoski-sequence.lagda.md b/src/elementary-number-theory/kolakoski-sequence.lagda.md
index fbc5410387..602bc2597a 100644
--- a/src/elementary-number-theory/kolakoski-sequence.lagda.md
+++ b/src/elementary-number-theory/kolakoski-sequence.lagda.md
@@ -20,7 +20,8 @@ open import foundation.dependent-pair-types
 
 ## Idea
 
-The Kolakoski sequence
+The
+{{#concept "Kolakoski sequence" WD="Kolakoski sequence" WDID=Q6427013 Agda=kolakoski}}
 
 ```text
 1,2,2,1,1,2,1,2,2,1,2,2,1,1,...
@@ -66,3 +67,7 @@ kolakoski n with pr1 (kolakoski-helper n)
 ... | true = 2
 ... | false = 1
 ```
+
+## External links
+
+- [A000002](https://oeis.org/A000002) in the OEIS
diff --git a/src/elementary-number-theory/legendre-symbol.lagda.md b/src/elementary-number-theory/legendre-symbol.lagda.md
index 142a859422..57f91cb937 100644
--- a/src/elementary-number-theory/legendre-symbol.lagda.md
+++ b/src/elementary-number-theory/legendre-symbol.lagda.md
@@ -24,7 +24,9 @@ open import foundation.identity-types
 
 ## Idea
 
-The **Legendre symbol** is a function which determines whether or not an
+The
+{{#concept "Legendre symbol" WD="Legendre symbol" WDID=Q748339 Agda=legendre-symbol}}
+is a function which determines whether or not an
 [integer](elementary-number-theory.integers.md) is a perfect square in the ring
 `ℤₚ` of [integers modulo `p`](elementary-number-theory.modular-arithmetic.md)
 (i.e. whether or not it is a quadratic residue). Specifically, let `p : Prime-ℕ`
diff --git a/src/elementary-number-theory/natural-numbers.lagda.md b/src/elementary-number-theory/natural-numbers.lagda.md
index 54c546f857..1b5591c183 100644
--- a/src/elementary-number-theory/natural-numbers.lagda.md
+++ b/src/elementary-number-theory/natural-numbers.lagda.md
@@ -21,9 +21,10 @@ open import foundation-core.negation
 
 ## Idea
 
-The **natural numbers** is an inductively generated type by the zero element and
-the successor function. The induction principle for the natural numbers works to
-construct sections of type families over the natural numbers.
+The {{#concept "natural numbers" WD="natural number" WDID=Q21199 Agda=ℕ}} is an
+inductively generated type by the zero element and the successor function. The
+induction principle for the natural numbers works to construct sections of type
+families over the natural numbers.
 
 ## Definitions
 
diff --git a/src/elementary-number-theory/peano-arithmetic.lagda.md b/src/elementary-number-theory/peano-arithmetic.lagda.md
index 25e87794d3..97139b2a63 100644
--- a/src/elementary-number-theory/peano-arithmetic.lagda.md
+++ b/src/elementary-number-theory/peano-arithmetic.lagda.md
@@ -159,4 +159,4 @@ peano-9-ℕ P = ind-ℕ {P = type-Prop ∘ P}
 - [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
-  Mathworld
+  MathWorld
diff --git a/src/elementary-number-theory/taxicab-numbers.lagda.md b/src/elementary-number-theory/taxicab-numbers.lagda.md
index 78c1cc32bf..6c89d1db21 100644
--- a/src/elementary-number-theory/taxicab-numbers.lagda.md
+++ b/src/elementary-number-theory/taxicab-numbers.lagda.md
@@ -101,4 +101,4 @@ is-taxicab-number-ℕ n x =
 ## External links
 
 - [Taxicab numbers](https://en.wikipedia.org/wiki/Taxicab_number) at Wikipedia
-- [Taxicab nubmers](https://oeis.org/A011541) at the OEIS.
+- [Taxicab numbers](https://oeis.org/A011541) in the OEIS.
diff --git a/src/elementary-number-theory/telephone-numbers.lagda.md b/src/elementary-number-theory/telephone-numbers.lagda.md
index 7269d3f6ed..61ecd7afe7 100644
--- a/src/elementary-number-theory/telephone-numbers.lagda.md
+++ b/src/elementary-number-theory/telephone-numbers.lagda.md
@@ -16,10 +16,11 @@ open import elementary-number-theory.natural-numbers
 
 ## Idea
 
-The telephone numbers are a sequence of natural numbers that count the way `n`
-telephone lines can be connected to each other, where each line can be connected
-to at most one other line. They also occur in several other combinatorics
-problems.
+The
+{{#concept "telephone numbers" WD="Telephone number" WDID=Q7696507 Agda=telephone-number}}
+are a sequence of natural numbers that count the way `n` telephone lines can be
+connected to each other, where each line can be connected to at most one other
+line. They also occur in several other combinatorics problems.
 
 ## Definitions
 
diff --git a/src/graph-theory/acyclic-undirected-graphs.lagda.md b/src/graph-theory/acyclic-undirected-graphs.lagda.md
index a1475aa0c5..300bd4eda8 100644
--- a/src/graph-theory/acyclic-undirected-graphs.lagda.md
+++ b/src/graph-theory/acyclic-undirected-graphs.lagda.md
@@ -68,4 +68,4 @@ is-acyclic-Undirected-Graph l G =
 - [Forests](<https://en.wikipedia.org/wiki/Tree_(graph_theory)#Forest>) at
   Wikipedia
 - [Acyclic graphs](https://mathworld.wolfram.com/AcyclicGraph.html) at Wolfram
-  Mathworld.
+  MathWorld.
diff --git a/src/graph-theory/circuits-undirected-graphs.lagda.md b/src/graph-theory/circuits-undirected-graphs.lagda.md
index 1025483a46..e3a8ea7dcc 100644
--- a/src/graph-theory/circuits-undirected-graphs.lagda.md
+++ b/src/graph-theory/circuits-undirected-graphs.lagda.md
@@ -48,4 +48,4 @@ module _
 - [Cycle (Graph Theory)](<https://en.wikipedia.org/wiki/Cycle_(graph_theory)>)
   at Wikipedia
 - [Graph Cycle](https://mathworld.wolfram.com/GraphCycle.html) at Wolfram
-  Mathworld
+  MathWorld
diff --git a/src/graph-theory/closed-walks-undirected-graphs.lagda.md b/src/graph-theory/closed-walks-undirected-graphs.lagda.md
index 5dc7938918..54484b5def 100644
--- a/src/graph-theory/closed-walks-undirected-graphs.lagda.md
+++ b/src/graph-theory/closed-walks-undirected-graphs.lagda.md
@@ -45,4 +45,4 @@ module _
 - [Cycle (Graph Theory)](<https://en.wikipedia.org/wiki/Cycle_(graph_theory)>)
   at Wikipedia
 - [Graph Cycle](https://mathworld.wolfram.com/GraphCycle.html) at Wolfram
-  Mathworld
+  MathWorld
diff --git a/src/graph-theory/complete-bipartite-graphs.lagda.md b/src/graph-theory/complete-bipartite-graphs.lagda.md
index aa3c3971e2..75c9a8d107 100644
--- a/src/graph-theory/complete-bipartite-graphs.lagda.md
+++ b/src/graph-theory/complete-bipartite-graphs.lagda.md
@@ -106,4 +106,4 @@ module _
 - [Complete bipartite graph](https://en.wikipedia.org/wiki/Complete_bipartite_graph)
   at Wikipedia
 - [Complete bipartite graphs](https://mathworld.wolfram.com/CompleteBipartiteGraph.html)
-  at Wolfram Mathworld
+  at Wolfram MathWorld
diff --git a/src/graph-theory/complete-multipartite-graphs.lagda.md b/src/graph-theory/complete-multipartite-graphs.lagda.md
index a98aa64ad9..77c362e968 100644
--- a/src/graph-theory/complete-multipartite-graphs.lagda.md
+++ b/src/graph-theory/complete-multipartite-graphs.lagda.md
@@ -94,4 +94,4 @@ module _
 - [Multipartite graph](https://en.wikipedia.org/wiki/Multipartite_graph) on
   Wikipedia
 - [Complete multipartite graph](https://mathworld.wolfram.com/CompleteMultipartiteGraph.html)
-  on Wolfram Mathworld
+  on Wolfram MathWorld
diff --git a/src/graph-theory/complete-undirected-graphs.lagda.md b/src/graph-theory/complete-undirected-graphs.lagda.md
index a4f8b58b73..693e6fdb3b 100644
--- a/src/graph-theory/complete-undirected-graphs.lagda.md
+++ b/src/graph-theory/complete-undirected-graphs.lagda.md
@@ -45,4 +45,4 @@ complete-Undirected-Graph-𝔽 X =
 - [Complete graph](https://www.wikidata.org/entity/Q45715) on Wikidata
 - [Complete graph](https://en.wikipedia.org/wiki/Complete_graph) on Wikipedia
 - [Complete graph](https://mathworld.wolfram.com/CompleteGraph.html) at Wolfram
-  Mathworld
+  MathWorld
diff --git a/src/graph-theory/connected-undirected-graphs.lagda.md b/src/graph-theory/connected-undirected-graphs.lagda.md
index 28b1dc2cb1..fafe80a55b 100644
--- a/src/graph-theory/connected-undirected-graphs.lagda.md
+++ b/src/graph-theory/connected-undirected-graphs.lagda.md
@@ -54,4 +54,4 @@ module _
 - [Connectivity (graph theory)](<https://en.wikipedia.org/wiki/Connectivity_(graph_theory)>)
   on Wikipedia
 - [Connected graph](https://mathworld.wolfram.com/ConnectedGraph.html) at
-  Wolfram Mathworld
+  Wolfram MathWorld
diff --git a/src/graph-theory/cycles-undirected-graphs.lagda.md b/src/graph-theory/cycles-undirected-graphs.lagda.md
index e152afc74a..2dd455a2f4 100644
--- a/src/graph-theory/cycles-undirected-graphs.lagda.md
+++ b/src/graph-theory/cycles-undirected-graphs.lagda.md
@@ -46,4 +46,4 @@ module _
 - [Cycle (graph theory)](<https://en.wikipedia.org/wiki/Cycle_(graph_theory)>)
   at Wikipedia
 - [Graph cycle](https://mathworld.wolfram.com/GraphCycle.html) at Wolfram
-  Mathworld
+  MathWorld
diff --git a/src/graph-theory/directed-graph-structures-on-standard-finite-sets.lagda.md b/src/graph-theory/directed-graph-structures-on-standard-finite-sets.lagda.md
index b7988be011..5cdafc94d7 100644
--- a/src/graph-theory/directed-graph-structures-on-standard-finite-sets.lagda.md
+++ b/src/graph-theory/directed-graph-structures-on-standard-finite-sets.lagda.md
@@ -63,4 +63,4 @@ Labeled-Finite-Directed-Graph = Σ ℕ (λ n → Fin n → Fin n → ℕ)
 - [Directed graph](https://www.wikidata.org/entity/Q1137726) on Wikdiata
 - [Directed graph](https://en.wikipedia.org/wiki/Directed_graph) at Wikipedia
 - [Directed graph](https://mathworld.wolfram.com/DirectedGraph.html) at Wolfram
-  Mathworld
+  MathWorld
diff --git a/src/graph-theory/directed-graphs.lagda.md b/src/graph-theory/directed-graphs.lagda.md
index 9e74e28643..64a2ceffa7 100644
--- a/src/graph-theory/directed-graphs.lagda.md
+++ b/src/graph-theory/directed-graphs.lagda.md
@@ -140,4 +140,4 @@ module equiv {l1 l2 : Level} where
 - [Directed graph](https://www.wikidata.org/entity/Q1137726) on Wikidata
 - [Directed graph](https://en.wikipedia.org/wiki/Directed_graph) at Wikipedia
 - [Directed graph](https://mathworld.wolfram.com/DirectedGraph.html) at Wolfram
-  Mathworld
+  MathWorld
diff --git a/src/graph-theory/edge-coloured-undirected-graphs.lagda.md b/src/graph-theory/edge-coloured-undirected-graphs.lagda.md
index 59bcfbb4c4..fe22d6bcf3 100644
--- a/src/graph-theory/edge-coloured-undirected-graphs.lagda.md
+++ b/src/graph-theory/edge-coloured-undirected-graphs.lagda.md
@@ -106,5 +106,5 @@ module _
 
 - [Edge coloring](https://en.wikipedia.org/wiki/Edge_coloring) at Wikipedia
 - [Edge coloring](https://mathworld.wolfram.com/EdgeColoring.html) at Wolfram
-  Mathworld
+  MathWorld
 - [Graph coloring](https://www.wikidata.org/entity/Q504843) on Wikidata
diff --git a/src/graph-theory/enriched-undirected-graphs.lagda.md b/src/graph-theory/enriched-undirected-graphs.lagda.md
index 606c964cb0..1f74332982 100644
--- a/src/graph-theory/enriched-undirected-graphs.lagda.md
+++ b/src/graph-theory/enriched-undirected-graphs.lagda.md
@@ -202,4 +202,4 @@ module _
 - [Graph](https://www.wikidata.org/entity/Q141488) on Wikidata
 - [Graph (discrete mathematics)](<https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)>)
   at Wikipedia
-- [Graph](https://mathworld.wolfram.com/Graph.html) at Wolfram Mathworld
+- [Graph](https://mathworld.wolfram.com/Graph.html) at Wolfram MathWorld
diff --git a/src/graph-theory/equivalences-directed-graphs.lagda.md b/src/graph-theory/equivalences-directed-graphs.lagda.md
index 327cdee91a..ac054fd589 100644
--- a/src/graph-theory/equivalences-directed-graphs.lagda.md
+++ b/src/graph-theory/equivalences-directed-graphs.lagda.md
@@ -533,5 +533,5 @@ module _
 - [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
   Wikipedia
 - [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
-  Wolfram Mathworld
+  Wolfram MathWorld
 - [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at $n$Lab
diff --git a/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md b/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md
index 635cd5b9f2..0c9b255d3a 100644
--- a/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md
+++ b/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md
@@ -250,5 +250,5 @@ module _
 - [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
   Wikipedia
 - [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
-  Wolfram Mathworld
+  Wolfram MathWorld
 - [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at $n$Lab
diff --git a/src/graph-theory/equivalences-undirected-graphs.lagda.md b/src/graph-theory/equivalences-undirected-graphs.lagda.md
index 4dc5daf15b..23b1135233 100644
--- a/src/graph-theory/equivalences-undirected-graphs.lagda.md
+++ b/src/graph-theory/equivalences-undirected-graphs.lagda.md
@@ -288,5 +288,5 @@ module _
 - [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
   Wikipedia
 - [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
-  Wolfram Mathworld
+  Wolfram MathWorld
 - [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at $n$Lab
diff --git a/src/graph-theory/hypergraphs.lagda.md b/src/graph-theory/hypergraphs.lagda.md
index 617e2dae80..018e504f13 100644
--- a/src/graph-theory/hypergraphs.lagda.md
+++ b/src/graph-theory/hypergraphs.lagda.md
@@ -48,4 +48,4 @@ module _
 - [Hypergraph](https://www.wikidata.org/entity/Q840247) on Wikidata
 - [Hypergraph](https://en.wikipedia.org/wiki/Hypergraph) at Wikipedia
 - [Hypergraph](https://mathworld.wolfram.com/Hypergraph.html) at Wolfram
-  Mathworld
+  MathWorld
diff --git a/src/graph-theory/large-reflexive-graphs.lagda.md b/src/graph-theory/large-reflexive-graphs.lagda.md
index 4b1a7ff71d..0885e859a1 100644
--- a/src/graph-theory/large-reflexive-graphs.lagda.md
+++ b/src/graph-theory/large-reflexive-graphs.lagda.md
@@ -52,4 +52,4 @@ open Large-Reflexive-Graph public
 - [Graph](https://www.wikidata.org/entity/Q141488) on Wikidata
 - [Directed graph](https://en.wikipedia.org/wiki/Directed_graph) at Wikipedia
 - [Reflexive graph](https://mathworld.wolfram.com/ReflexiveGraph.html) at
-  Wolfram Mathworld
+  Wolfram MathWorld
diff --git a/src/graph-theory/matchings.lagda.md b/src/graph-theory/matchings.lagda.md
index 50d7b8d9b4..66d2d1cc2c 100644
--- a/src/graph-theory/matchings.lagda.md
+++ b/src/graph-theory/matchings.lagda.md
@@ -68,4 +68,4 @@ module _
 - [Matching](https://www.wikidata.org/entity/Q1065144) on Wikidata
 - [Matching (graph theory)](<https://en.wikipedia.org/wiki/Matching_(graph_theory)>)
   at Wikipedia
-- [Matching](https://mathworld.wolfram.com/Matching.html) at Wolfram Mathworld
+- [Matching](https://mathworld.wolfram.com/Matching.html) at Wolfram MathWorld
diff --git a/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md b/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md
index 6b24f77c48..9376ae4058 100644
--- a/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md
+++ b/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md
@@ -64,5 +64,5 @@ module _
 - [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
   Wikipedia
 - [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
-  Wolfram Mathworld
+  Wolfram MathWorld
 - [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at $n$Lab
diff --git a/src/graph-theory/neighbors-undirected-graphs.lagda.md b/src/graph-theory/neighbors-undirected-graphs.lagda.md
index 54548de3ad..4e88fc790e 100644
--- a/src/graph-theory/neighbors-undirected-graphs.lagda.md
+++ b/src/graph-theory/neighbors-undirected-graphs.lagda.md
@@ -86,4 +86,4 @@ neighbor-id-equiv-Undirected-Graph G x (pair y e) =
 - [Neighborhood (graph theory)](<https://en.wikipedia.org/wiki/Neighbourhood_(graph_theory)>)
   at Wikipedia
 - [Graph neighborhood](https://mathworld.wolfram.com/GraphNeighborhood.html) at
-  Wolfram Mathworld
+  Wolfram MathWorld
diff --git a/src/graph-theory/orientations-undirected-graphs.lagda.md b/src/graph-theory/orientations-undirected-graphs.lagda.md
index 56419d0977..addaff4781 100644
--- a/src/graph-theory/orientations-undirected-graphs.lagda.md
+++ b/src/graph-theory/orientations-undirected-graphs.lagda.md
@@ -48,4 +48,4 @@ module _
 - [Orientation (graph theory)](<https://en.wikipedia.org/wiki/Orientation_(graph_theory)>)
   at Wikipedia
 - [Graph orientation](https://mathworld.wolfram.com/GraphOrientation.html) at
-  Wolfram Mathworld
+  Wolfram MathWorld
diff --git a/src/graph-theory/paths-undirected-graphs.lagda.md b/src/graph-theory/paths-undirected-graphs.lagda.md
index 4241b42108..b811c34281 100644
--- a/src/graph-theory/paths-undirected-graphs.lagda.md
+++ b/src/graph-theory/paths-undirected-graphs.lagda.md
@@ -82,4 +82,4 @@ is-path-refl-walk-Undirected-Graph G x =
 - [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
   Wikipedia
 - [Graph path](https://mathworld.wolfram.com/GraphPath.html) at Wolfram
-  Mathworld
+  MathWorld
diff --git a/src/graph-theory/polygons.lagda.md b/src/graph-theory/polygons.lagda.md
index 5224b39ed3..e77e88aefd 100644
--- a/src/graph-theory/polygons.lagda.md
+++ b/src/graph-theory/polygons.lagda.md
@@ -149,4 +149,4 @@ This remains to be formalized.
 - [Cycle graph](https://www.wikidata.org/entity/Q622506) on Wikidata
 - [Cycle graph](https://en.wikipedia.org/wiki/Cycle_graph) at Wikipedia
 - [Cycle graph](https://mathworld.wolfram.com/CycleGraph.html) at Wolfram
-  Mathworld
+  MathWorld
diff --git a/src/graph-theory/reflexive-graphs.lagda.md b/src/graph-theory/reflexive-graphs.lagda.md
index bc0a4e872b..76f15912ae 100644
--- a/src/graph-theory/reflexive-graphs.lagda.md
+++ b/src/graph-theory/reflexive-graphs.lagda.md
@@ -55,4 +55,4 @@ module _
 - [Graph](https://www.wikidata.org/entity/Q141488) on Wikidata
 - [Directed graph](https://en.wikipedia.org/wiki/Directed_graph) at Wikipedia
 - [Reflexive graph](https://mathworld.wolfram.com/ReflexiveGraph.html) at
-  Wolfram Mathworld
+  Wolfram MathWorld
diff --git a/src/graph-theory/regular-undirected-graphs.lagda.md b/src/graph-theory/regular-undirected-graphs.lagda.md
index 8b64834fa1..295ec95081 100644
--- a/src/graph-theory/regular-undirected-graphs.lagda.md
+++ b/src/graph-theory/regular-undirected-graphs.lagda.md
@@ -54,4 +54,4 @@ is-prop-is-regular-Undirected-Graph X G =
 - [Regular graph](https://www.wikidata.org/entity/Q826467) on Wikidata
 - [Regular graph](https://en.wikipedia.org/wiki/Regular_graph) at Wikipedia
 - [Regular graph](https://mathworld.wolfram.com/RegularGraph.html) at Wolfram
-  Mathworld
+  MathWorld
diff --git a/src/graph-theory/simple-undirected-graphs.lagda.md b/src/graph-theory/simple-undirected-graphs.lagda.md
index eff1724486..f2ed3e728c 100644
--- a/src/graph-theory/simple-undirected-graphs.lagda.md
+++ b/src/graph-theory/simple-undirected-graphs.lagda.md
@@ -72,4 +72,4 @@ Simple-Undirected-Graph l1 l2 =
   at Wikipedia
 - [Simple graph](https://www.wikidata.org/entity/Q15838309) on Wikidata
 - [Simple graph](https://mathworld.wolfram.com/SimpleGraph.html) at Wolfram
-  Mathworld
+  MathWorld
diff --git a/src/graph-theory/trails-directed-graphs.lagda.md b/src/graph-theory/trails-directed-graphs.lagda.md
index f3a179f25f..19c803955e 100644
--- a/src/graph-theory/trails-directed-graphs.lagda.md
+++ b/src/graph-theory/trails-directed-graphs.lagda.md
@@ -53,4 +53,4 @@ module _
 - [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
   Wikipedia
 - [Trail](https://www.wikidata.org/entity/Q17455228) on Wikidata
-- [Trail](https://mathworld.wolfram.com/Trail.html) at Wolfram Mathworld
+- [Trail](https://mathworld.wolfram.com/Trail.html) at Wolfram MathWorld
diff --git a/src/graph-theory/trails-undirected-graphs.lagda.md b/src/graph-theory/trails-undirected-graphs.lagda.md
index b26efaa0cb..3aaaa397cc 100644
--- a/src/graph-theory/trails-undirected-graphs.lagda.md
+++ b/src/graph-theory/trails-undirected-graphs.lagda.md
@@ -166,4 +166,4 @@ module _
 - [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
   Wikipedia
 - [Trail](https://www.wikidata.org/entity/Q17455228) on Wikidata
-- [Trail](https://mathworld.wolfram.com/Trail.html) at Wolfram Mathworld
+- [Trail](https://mathworld.wolfram.com/Trail.html) at Wolfram MathWorld
diff --git a/src/graph-theory/undirected-graph-structures-on-standard-finite-sets.lagda.md b/src/graph-theory/undirected-graph-structures-on-standard-finite-sets.lagda.md
index d1684f4fb1..b16324d61e 100644
--- a/src/graph-theory/undirected-graph-structures-on-standard-finite-sets.lagda.md
+++ b/src/graph-theory/undirected-graph-structures-on-standard-finite-sets.lagda.md
@@ -31,4 +31,4 @@ Undirected-Graph-Fin = Σ ℕ (λ V → unordered-pair (Fin V) → ℕ)
 - [Graph](https://www.wikidata.org/entity/Q141488) on Wikidata
 - [Graph (discrete mathematics)](<https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)>)
   at Wikipedia
-- [Graph](https://mathworld.wolfram.com/Graph.html) at Wolfram Mathworld
+- [Graph](https://mathworld.wolfram.com/Graph.html) at Wolfram MathWorld
diff --git a/src/graph-theory/undirected-graphs.lagda.md b/src/graph-theory/undirected-graphs.lagda.md
index 7829e1143e..dda08c3492 100644
--- a/src/graph-theory/undirected-graphs.lagda.md
+++ b/src/graph-theory/undirected-graphs.lagda.md
@@ -122,4 +122,4 @@ module _
 - [Graph](https://www.wikidata.org/entity/Q141488) on Wikidata
 - [Graph (discrete mathematics)](<https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)>)
   at Wikipedia
-- [Graph](https://mathworld.wolfram.com/Graph.html) at Wolfram Mathworld
+- [Graph](https://mathworld.wolfram.com/Graph.html) at Wolfram MathWorld
diff --git a/src/graph-theory/vertex-covers.lagda.md b/src/graph-theory/vertex-covers.lagda.md
index f074369851..462cda70c8 100644
--- a/src/graph-theory/vertex-covers.lagda.md
+++ b/src/graph-theory/vertex-covers.lagda.md
@@ -47,5 +47,5 @@ vertex-cover G =
 
 - [Vertex cover](https://en.wikipedia.org/wiki/Vertex_cover) at Wikipedia
 - [Vertex cover](https://mathworld.wolfram.com/VertexCover.html) at Wolfram
-  Mathworld
+  MathWorld
 - [Vertex cover problem](https://www.wikidata.org/entity/Q924362) on Wikidata
diff --git a/src/graph-theory/walks-directed-graphs.lagda.md b/src/graph-theory/walks-directed-graphs.lagda.md
index cc52281587..22af690b4f 100644
--- a/src/graph-theory/walks-directed-graphs.lagda.md
+++ b/src/graph-theory/walks-directed-graphs.lagda.md
@@ -785,4 +785,4 @@ module _
 - [Path](https://www.wikidata.org/entity/Q917421) on Wikidata
 - [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
   Wikipedia
-- [Walk](https://mathworld.wolfram.com/Walk.html) at Wolfram Mathworld
+- [Walk](https://mathworld.wolfram.com/Walk.html) at Wolfram MathWorld
diff --git a/src/graph-theory/walks-undirected-graphs.lagda.md b/src/graph-theory/walks-undirected-graphs.lagda.md
index 69382fdfdb..c58e06ebf8 100644
--- a/src/graph-theory/walks-undirected-graphs.lagda.md
+++ b/src/graph-theory/walks-undirected-graphs.lagda.md
@@ -520,4 +520,4 @@ module _
 - [Path](https://www.wikidata.org/entity/Q917421) on Wikidata
 - [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
   Wikipedia
-- [Walk](https://mathworld.wolfram.com/Walk.html) at Wolfram Mathworld
+- [Walk](https://mathworld.wolfram.com/Walk.html) at Wolfram MathWorld
diff --git a/src/group-theory/abelianization-groups.lagda.md b/src/group-theory/abelianization-groups.lagda.md
index 777127d7e1..5698ee542f 100644
--- a/src/group-theory/abelianization-groups.lagda.md
+++ b/src/group-theory/abelianization-groups.lagda.md
@@ -442,4 +442,4 @@ is-adjoint-pair-Adjunction-Large-Precategory
 - [Abelianization](https://en.wikipedia.org/wiki/Commutator_subgroup#Abelianization)
   at Wikipedia
 - [Abelianization](https://mathworld.wolfram.com/Abelianization.html) at Wolfram
-  Mathworld
+  MathWorld
diff --git a/src/group-theory/commutator-subgroups.lagda.md b/src/group-theory/commutator-subgroups.lagda.md
index 2316c49c7e..1300e1e9be 100644
--- a/src/group-theory/commutator-subgroups.lagda.md
+++ b/src/group-theory/commutator-subgroups.lagda.md
@@ -218,4 +218,4 @@ module _
 - [Commutator subgroup](https://en.wikipedia.org/wiki/Commutator_subgroup) at
   Wikipedia
 - [Commutator subgroup](https://mathworld.wolfram.com/CommutatorSubgroup.html)
-  at Wolfram Mathworld
+  at Wolfram MathWorld
diff --git a/src/group-theory/commutators-of-elements-groups.lagda.md b/src/group-theory/commutators-of-elements-groups.lagda.md
index faf2370475..086b8fcc4d 100644
--- a/src/group-theory/commutators-of-elements-groups.lagda.md
+++ b/src/group-theory/commutators-of-elements-groups.lagda.md
@@ -140,5 +140,5 @@ module _
 - [Commutator](https://en.wikipedia.org/wiki/Commutator#Group_theory) at
   Wikipedia
 - [Commutator](https://mathworld.wolfram.com/Commutator.html) at Wolfram
-  Mathworld
+  MathWorld
 - [Group commutator](https://ncatlab.org/nlab/show/group+commutator) at $n$Lab
diff --git a/src/group-theory/stabilizer-groups-concrete-group-actions.lagda.md b/src/group-theory/stabilizer-groups-concrete-group-actions.lagda.md
index 68c7239768..fccff9b2a3 100644
--- a/src/group-theory/stabilizer-groups-concrete-group-actions.lagda.md
+++ b/src/group-theory/stabilizer-groups-concrete-group-actions.lagda.md
@@ -91,6 +91,6 @@ module _
 - [Fixed points and stabilizer subgroups](https://en.wikipedia.org/wiki/Group_action#Fixed_points_and_stabilizer_subgroups)
   at Wikipedia
 - [Isotropy Group](https://mathworld.wolfram.com/IsotropyGroup.html) at Wolfram
-  Mathworld
+  MathWorld
 - [Isotropy group](https://encyclopediaofmath.org/wiki/Isotropy_group) at
   Encyclopedia of Mathematics
diff --git a/src/group-theory/stabilizer-groups.lagda.md b/src/group-theory/stabilizer-groups.lagda.md
index e5f439da59..6786bf463a 100644
--- a/src/group-theory/stabilizer-groups.lagda.md
+++ b/src/group-theory/stabilizer-groups.lagda.md
@@ -41,6 +41,6 @@ module _
 - [Fixed points and stabilizer subgroups](https://en.wikipedia.org/wiki/Group_action#Fixed_points_and_stabilizer_subgroups)
   at Wikipedia
 - [Isotropy Group](https://mathworld.wolfram.com/IsotropyGroup.html) at Wolfram
-  Mathworld
+  MathWorld
 - [Isotropy group](https://encyclopediaofmath.org/wiki/Isotropy_group) at
   Encyclopedia of Mathematics
diff --git a/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md b/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
index 364ee7abc8..af6d989e10 100644
--- a/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
+++ b/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
@@ -8,6 +8,7 @@ module online-encyclopedia-of-integer-sequences.oeis where
 
 ```agda
 open import elementary-number-theory.ackermann-function
+open import elementary-number-theory.catalan-numbers
 open import elementary-number-theory.cofibonacci
 open import elementary-number-theory.collatz-bijection
 open import elementary-number-theory.eulers-totient-function
@@ -24,6 +25,8 @@ open import elementary-number-theory.pisano-periods
 open import finite-group-theory.finite-groups
 
 open import foundation.function-types
+
+open import univalent-combinatorics.main-classes-of-latin-squares
 ```
 
 </details>
@@ -101,6 +104,13 @@ A000079 : ℕ → ℕ
 A000079 = exp-ℕ 2
 ```
 
+### [A000108](https://oeis.org/A000108) The Catalan numbers
+
+```agda
+A000108 : ℕ → ℕ
+A000108 = catalan-numbers
+```
+
 ### [A000142](https://oeis.org/A000142) Factorials
 
 ```agda
@@ -150,6 +160,13 @@ A001477 : ℕ → ℕ
 A001477 = id
 ```
 
+### [A003090](https://oeis.org/A003090) The natural numbers
+
+```agda
+A003090 : ℕ → ℕ
+A003090 = number-of-main-classes-of-Latin-squares-of-order
+```
+
 ### [A006369](https://oeis.org/A006369) Collatz' bijection
 
 ```agda
diff --git a/src/univalent-combinatorics/binomial-types.lagda.md b/src/univalent-combinatorics/binomial-types.lagda.md
index e08d5d666f..67fa86bce3 100644
--- a/src/univalent-combinatorics/binomial-types.lagda.md
+++ b/src/univalent-combinatorics/binomial-types.lagda.md
@@ -59,7 +59,8 @@ open import univalent-combinatorics.standard-finite-types
 ## Idea
 
 The {{#concept "binomial types" Agda=binomial-type}} are a categorification of
-the binomial coefficients. The binomial type `(A choose B)` is the type of
+the [binomial coefficients](elementary-number-theory.binomial-coefficients.md).
+The binomial type `(A choose B)` is the type of
 [decidable embeddings](foundation.decidable-embeddings.md) from types
 [merely equivalent](foundation.mere-equivalences.md) to `B` into `A`.
 

From e059dc9bcf9df3949f7eb961cb25ce8cf6ab434a Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 16 Oct 2024 16:52:00 +0200
Subject: [PATCH 2/4] fix header

---
 src/online-encyclopedia-of-integer-sequences/oeis.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md b/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
index af6d989e10..3ac9a75c21 100644
--- a/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
+++ b/src/online-encyclopedia-of-integer-sequences/oeis.lagda.md
@@ -160,7 +160,7 @@ A001477 : ℕ → ℕ
 A001477 = id
 ```
 
-### [A003090](https://oeis.org/A003090) The natural numbers
+### [A003090](https://oeis.org/A003090) The number of main classes of Latin squares of order `n`
 
 ```agda
 A003090 : ℕ → ℕ

From 97d847934df6b464c16ba47c3827a34384fc8b51 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 16 Oct 2024 17:05:39 +0200
Subject: [PATCH 3/4] distance

---
 src/elementary-number-theory/catalan-numbers.lagda.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/elementary-number-theory/catalan-numbers.lagda.md b/src/elementary-number-theory/catalan-numbers.lagda.md
index ccec4a8716..55a1c2eb40 100644
--- a/src/elementary-number-theory/catalan-numbers.lagda.md
+++ b/src/elementary-number-theory/catalan-numbers.lagda.md
@@ -80,8 +80,8 @@ catalan-numbers =
 
 ### Binomial difference formula for the Catalan numbers
 
-The Catalan numbers may be computed as a difference of consecutive binomial
-coefficients
+The Catalan numbers may be computed as a distance between two consecutive
+binomial coefficients
 
 $$
 C_n = {2n \choose n} - {2n \choose n + 1}.

From 6ee4a0762a16ed8ba660b165bc07d5e588d7e6a1 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 16 Oct 2024 17:14:45 +0200
Subject: [PATCH 4/4] distance explanation

---
 .../catalan-numbers.lagda.md                     | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/elementary-number-theory/catalan-numbers.lagda.md b/src/elementary-number-theory/catalan-numbers.lagda.md
index 55a1c2eb40..55257b4c79 100644
--- a/src/elementary-number-theory/catalan-numbers.lagda.md
+++ b/src/elementary-number-theory/catalan-numbers.lagda.md
@@ -80,13 +80,25 @@ catalan-numbers =
 
 ### Binomial difference formula for the Catalan numbers
 
-The Catalan numbers may be computed as a distance between two consecutive
-binomial coefficients
+The Catalan numbers may be computed as a
+[distance](elementary-number-theory.distance-natural-numbers.md) between two
+consecutive binomial coefficients
+
+$$
+C_n = \lvert{2n \choose n} - {2n \choose n + 1}\rvert.
+$$
+
+Since ${2n \choose n}$ in general is larger than or equal to
+${2n \choose n + 1}$, this distance is equal to the difference
 
 $$
 C_n = {2n \choose n} - {2n \choose n + 1}.
 $$
 
+However, we prefer the use of the distance binary operation on natural numbers
+in general at it is a total function on natural numbers, and allows us to skip
+proving this inequality.
+
 ```agda
 catalan-numbers-binomial : ℕ → ℕ
 catalan-numbers-binomial n =