UniMath · fredrik-bakke · Feb 14, 2025 · Feb 13, 2025 · Feb 13, 2025 · Feb 13, 2025
diff --git a/src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md b/src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md
@@ -40,7 +40,7 @@ The **binomial theorem** in commutative rings asserts that for any two elements
 ```
 
 The binomial theorem is the 44th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

diff --git a/src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md b/src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md
@@ -40,7 +40,7 @@ we have
 ```
 
 The binomial theorem is the 44th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

diff --git a/src/elementary-number-theory/bezouts-lemma-integers.lagda.md b/src/elementary-number-theory/bezouts-lemma-integers.lagda.md
@@ -39,7 +39,7 @@ open import foundation.unit-type
 </details>
 
 Bézout's Lemma is the 60th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}. It was
 originally added to agda-unimath by [Bryan Lu](https://blu-bird.github.io).
 

diff --git a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md b/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md
@@ -62,7 +62,7 @@ is decidable, because `P z ⇔ [y]_x | [z]_x` in `ℤ/x`. The least positive `z`
 such that `P z` holds is `gcd x y`.
 
 Bézout's Lemma is the 60th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}. It was
 originally added to agda-unimath by [Bryan Lu](https://blu-bird.github.io).
 

diff --git a/src/elementary-number-theory/binomial-theorem-integers.lagda.md b/src/elementary-number-theory/binomial-theorem-integers.lagda.md
@@ -37,7 +37,7 @@ The binomial theorem for the integers asserts that for any two integers `x` and
 ```
 
 The binomial theorem is the 44th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

diff --git a/src/elementary-number-theory/binomial-theorem-natural-numbers.lagda.md b/src/elementary-number-theory/binomial-theorem-natural-numbers.lagda.md
@@ -36,7 +36,7 @@ numbers `x` and `y` and any natural number `n`, we have
 ```
 
 The binomial theorem is the 44th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

diff --git a/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md b/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md
@@ -76,7 +76,7 @@ Note that the [univalence axiom](foundation-core.univalence.md) is neccessary to
 prove the second uniqueness property of prime factorizations.
 
 The fundamental theorem of arithmetic is the 80th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

diff --git a/src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md b/src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md
@@ -43,7 +43,7 @@ The greatest common divisor of two natural numbers `x` and `y` is a number
 `y` if and only if it is a divisor of `gcd x y`.
 
 The algorithm defining the greatest common divisor is the 69th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definition

diff --git a/src/elementary-number-theory/infinitude-of-primes.lagda.md b/src/elementary-number-theory/infinitude-of-primes.lagda.md
@@ -45,7 +45,7 @@ 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`.
 
 The infinitude of primes is the 11th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definition

diff --git a/src/elementary-number-theory/natural-numbers.lagda.md b/src/elementary-number-theory/natural-numbers.lagda.md
@@ -84,7 +84,7 @@ is-not-one-ℕ' n = ¬ (is-one-ℕ' n)
 ### The induction principle of ℕ
 
 The induction principle of the natural numbers is the 74th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ```agda

diff --git a/src/elementary-number-theory/rational-numbers.lagda.md b/src/elementary-number-theory/rational-numbers.lagda.md
@@ -206,7 +206,7 @@ retract-integer-fraction-ℚ =
 ### The rationals are countable
 
 The denumerability of the rational numbers is the third theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ```agda

diff --git a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md
@@ -39,7 +39,7 @@ Escardó proved that a Cantor–Schröder–Bernstein theorem also holds for
 [equivalent](foundation-core.equivalences.md). {{#cite Esc21}}
 
 The Cantor–Schröder–Bernstein theorem is the 25th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Statement

diff --git a/src/foundation/cantors-theorem.lagda.md b/src/foundation/cantors-theorem.lagda.md
@@ -63,7 +63,7 @@ would have to be a fixed point of the negation operation, since
 but negation has no fixed points.
 
 Cantor's theorem is the 63rd theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ```agda

diff --git a/src/literature/100-theorems.lagda.md b/src/literature/100-theorems.lagda.md
@@ -1,7 +1,7 @@
 # Freek Wiedijk's 100 Theorems
 
 This file records formalized results from
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/)
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s
 [_Formalizing 100 Theorems_](https://www.cs.ru.nl/~freek/100/).
 {{#cite 100theorems}}
 
@@ -11,7 +11,7 @@ module literature.100-theorems where
 
 ## The list
 
-### [3. The Denumerability of the Rational Numbers](https://www.cs.ru.nl/~freek/100/#3) {#3}
+### 3. The Denumerability of the Rational Numbers [(#3)](https://www.cs.ru.nl/~freek/100/#3) {#3}
 
 **Author:** [Fredrik Bakke](https://www.ntnu.edu/employees/fredrik.bakke)
 
@@ -20,7 +20,7 @@ open import elementary-number-theory.rational-numbers using
   ( is-countable-ℚ)
 ```
 
-### [11. The Infinitude of Primes](https://www.cs.ru.nl/~freek/100/#11) {#11}
+### 11. The Infinitude of Primes [(#11)](https://www.cs.ru.nl/~freek/100/#11) {#11}
 
 **Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
@@ -29,11 +29,11 @@ open import elementary-number-theory.infinitude-of-primes using
   ( infinitude-of-primes-ℕ)
 ```
 
-### [22. The Non-Denumerability of the Continuum](https://www.cs.ru.nl/~freek/100/#22) {#22}
+### 22. The Non-Denumerability of the Continuum [(#22)](https://www.cs.ru.nl/~freek/100/#22) {#22}
 
 > This is not yet formalized.
 
-### [25. Schröder–Bernstein Theorem](https://www.cs.ru.nl/~freek/100/#25) {#25}
+### 25. Schröder–Bernstein Theorem [(#25)](https://www.cs.ru.nl/~freek/100/#25) {#25}
 
 **Author:** [Elif Uskuplu](https://elifuskuplu.github.io)
 
@@ -49,7 +49,7 @@ open import foundation.cantor-schroder-bernstein-escardo using
   ( Cantor-Schröder-Bernstein)
 ```
 
-### [44. The Binomial Theorem](https://www.cs.ru.nl/~freek/100/#44) {#44}
+### 44. The Binomial Theorem [(#44)](https://www.cs.ru.nl/~freek/100/#44) {#44}
 
 **Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
@@ -68,7 +68,7 @@ open import elementary-number-theory.binomial-theorem-natural-numbers using
   ( binomial-theorem-ℕ)
 ```
 
-### [52. The Number of Subsets of a Set](https://www.cs.ru.nl/~freek/100/#52) {#52}
+### 52. The Number of Subsets of a Set [(#52)](https://www.cs.ru.nl/~freek/100/#52) {#52}
 
 **Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
@@ -77,7 +77,7 @@ open import univalent-combinatorics.decidable-subtypes using
   ( number-of-elements-decidable-subtype-is-finite)
 ```
 
-### [58. Formula for the number of combinations](https://www.cs.ru.nl/~freek/100/#58) {#58}
+### 58. Formula for the number of combinations [(#58)](https://www.cs.ru.nl/~freek/100/#58) {#58}
 
 **Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
@@ -86,7 +86,7 @@ open import univalent-combinatorics.binomial-types using
   ( has-cardinality-binomial-type)
 ```
 
-### [60. Bezout's Lemma](https://www.cs.ru.nl/~freek/100/#60) {#60}
+### 60. Bezout's Lemma [(#60)](https://www.cs.ru.nl/~freek/100/#60) {#60}
 
 **Author:** [Bryan Lu](https://blu-bird.github.io)
 
@@ -101,7 +101,7 @@ open import elementary-number-theory.bezouts-lemma-natural-numbers using
   ( bezouts-lemma-ℕ)
 ```
 
-### [63. Cantor's Theorem](https://www.cs.ru.nl/~freek/100/#63) {#63}
+### 63. Cantor's Theorem [(#63)](https://www.cs.ru.nl/~freek/100/#63) {#63}
 
 **Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
@@ -110,7 +110,7 @@ open import foundation.cantors-theorem using
   ( theorem-Cantor)
 ```
 
-### [69. Greatest Common Divisor Algorithm](https://www.cs.ru.nl/~freek/100/#69) {#69}
+### 69. Greatest Common Divisor Algorithm [(#69)](https://www.cs.ru.nl/~freek/100/#69) {#69}
 
 **Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
@@ -120,7 +120,7 @@ open import
   ( GCD-ℕ)
 ```
 
-### [74. The Principle of Mathematical Induction](https://www.cs.ru.nl/~freek/100/#74) {#74}
+### 74. The Principle of Mathematical Induction [(#74)](https://www.cs.ru.nl/~freek/100/#74) {#74}
 
 **Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
@@ -129,7 +129,7 @@ open import elementary-number-theory.natural-numbers using
   ( ind-ℕ)
 ```
 
-### [80. The Fundamental Theorem of Arithmetic](https://www.cs.ru.nl/~freek/100/#80) {#80}
+### 80. The Fundamental Theorem of Arithmetic [(#80)](https://www.cs.ru.nl/~freek/100/#80) {#80}
 
 **Author:** [Victor Blanchi](https://github.com/VictorBlanchi)
 
@@ -138,7 +138,7 @@ open import elementary-number-theory.fundamental-theorem-of-arithmetic using
   ( fundamental-theorem-arithmetic-list-ℕ)
 ```
 
-### [91. The Triangle Inequality](https://www.cs.ru.nl/~freek/100/#91) {#91}
+### 91. The Triangle Inequality [(#91)](https://www.cs.ru.nl/~freek/100/#91) {#91}
 
 **Author:** [malarbol](https://github.com/malarbol)
 
@@ -147,7 +147,7 @@ open import real-numbers.metric-space-of-real-numbers using
   ( is-triangular-premetric-leq-ℝ)
 ```
 
-### [96. Principle of Inclusion/Exclusion](https://www.cs.ru.nl/~freek/100/#96) {#96}
+### 96. Principle of Inclusion/Exclusion [(#96)](https://www.cs.ru.nl/~freek/100/#96) {#96}
 
 > This is not yet formalized.
 

diff --git a/src/real-numbers/metric-space-of-real-numbers.lagda.md b/src/real-numbers/metric-space-of-real-numbers.lagda.md
@@ -99,7 +99,7 @@ premetric-leq-ℝ l d x y =
 ### The standard premetric on the real numbers is a metric structure
 
 The triangle inequality is the 91st theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ```agda

diff --git a/src/ring-theory/binomial-theorem-rings.lagda.md b/src/ring-theory/binomial-theorem-rings.lagda.md
@@ -39,7 +39,7 @@ have
 ```
 
 The binomial theorem is the 44th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

diff --git a/src/ring-theory/binomial-theorem-semirings.lagda.md b/src/ring-theory/binomial-theorem-semirings.lagda.md
@@ -42,7 +42,7 @@ have
 ```
 
 The binomial theorem is the 44th theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

diff --git a/src/univalent-combinatorics/binomial-types.lagda.md b/src/univalent-combinatorics/binomial-types.lagda.md
@@ -388,7 +388,7 @@ equiv-binomial-type e f =
 ### Computation of the number of elements of the binomial type `((Fin n) (Fin m))`
 
 The computation of the number of subsets of a given cardinality of a finite set
-is the 58th theorem on [Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+is the 58th theorem on [Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ```agda

diff --git a/src/univalent-combinatorics/decidable-subtypes.lagda.md b/src/univalent-combinatorics/decidable-subtypes.lagda.md
@@ -95,7 +95,7 @@ module _
 ### The type of decidable subtypes of a finite type is finite
 
 The computation of the number of subsets of a finite sets is the 52nd theorem on
-[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ```agda