Linked names (#1216)

UniMath · Oct 29, 2024 · 15d937a · 15d937a
1 parent e0eacab
commit 15d937a
Show file tree

Hide file tree

Showing 22 changed files with 86 additions and 56 deletions.
diff --git a/CONTRIBUTORS.toml b/CONTRIBUTORS.toml
@@ -12,10 +12,10 @@ displayName = "Egbert Rijke"
 maintainer = true
 extra = " (Lead developer)"
 usernames = [ "Egbert Rijke" ]
-homepage = "https://users.fmf.uni-lj.si/rijke/"
+homepage = "https://egbertrijke.github.io"
 github = "EgbertRijke"
 bio = '''
-Egbert Rijke is a postdoctoral researcher at the University of Ljubljana. His
+Egbert Rijke is a postdoctoral researcher at Johns Hopkins University. His
 research is on homotopy type theory and general mathematics from a univalent
 point of view.
 '''
@@ -75,16 +75,19 @@ github = "EleonoreMangel"
 displayName = "Bryan Lu"
 usernames = [ "Bryan Lu" ]
 github = "blu-bird"
+homepage = "https://blu-bird.github.io"
 
 [[contributors]]
 displayName = "Raymond Baker"
 usernames = [ "Raymond Baker" ]
 github = "morphismz"
+homepage = "https://morphismz.github.io"
 
 [[contributors]]
 displayName = "Elif Uskuplu"
 usernames = [ "ElifUskuplu" ]
 github = "ElifUskuplu"
+homepage = "https://elifuskuplu.github.io"
 
 [[contributors]]
 displayName = "Victor Blanchi"
@@ -149,6 +152,7 @@ usernames = [ "Julian KG" ]
 displayName = "favonia"
 usernames = [ "favonia" ]
 github = "favonia"
+homepage = "https://favonia.org"
 
 [[contributors]]
 displayName = "fernabnor"
@@ -217,6 +221,7 @@ github = "louismntnu"
 displayName = "Andrej Bauer"
 usernames = [ "Andrej Bauer" ]
 github = "andrejbauer"
+homepage = "https://www.andrej.com"
 
 [[contributors]]
 displayName = "Matej Petković"

diff --git a/HOME.md b/HOME.md
@@ -8,14 +8,18 @@ typed programming language [Agda](https://github.com/agda/agda).
 <img class="invertible-image" align="right" width="300" alt="agda-unimath" src="website/images/agda-unimath-logo.svg" />
 </a>
 
-The library project was created by Elisabeth Stenholm, Jonathan Prieto-Cubides,
-and Egbert Rijke, and is currently being maintained by Egbert Rijke, Fredrik
-Bakke, and Vojtěch Štěpančík. Our goal is to create an online encyclopedia of
-formalized mathematics containing an extensive curriculum of topics from a
-univalent point of view. We think libraries of formalized mathematics have the
-potential to be useful, and informative resources for both working and learning
-mathematicians. Our library is designed to work towards this goal, and we
-welcome contributions to the library within any topic in mathematics.
+The library project was created by
+[Elisabeth Stenholm](https://elisabeth.bonnevier.one),
+[Jonathan Prieto-Cubides](https://jonaprieto.github.io), and
+[Egbert Rijke](https://egbertrijke.github.io), and is currently being maintained
+by Egbert Rijke, [Fredrik Bakke](https://www.ntnu.edu/employees/fredrik.bakke),
+and [Vojtěch Štěpančík](https://vojtechstep.eu/). Our goal is to create an
+online encyclopedia of formalized mathematics containing an extensive curriculum
+of topics from a univalent point of view. We think libraries of formalized
+mathematics have the potential to be useful, and informative resources for both
+working and learning mathematicians. Our library is designed to work towards
+this goal, and we welcome contributions to the library within any topic in
+mathematics.
 
 The agda-unimath library is compatible with Agda 2.6.4 and can be compiled by
 running `make check` from the root directory of the repository. Learn more about

diff --git a/README.md b/README.md
@@ -2,13 +2,16 @@
 
 The agda-unimath library is a community formalization project for univalent
 mathematics in [Agda](https://github.com/agda/agda). The library project was
-created by Elisabeth Stenholm, Jonathan Prieto-Cubides, and Egbert Rijke, and is
-currently being maintained by Egbert Rijke, Fredrik Bakke, and Vojtěch
-Štěpančík. Our goal is to formalize an extensive curriculum of mathematics from
-the univalent point of view. Furthermore, we think libraries of formalized
-mathematics have the potential to be useful, and informative resources for
-mathematicians. Our library is designed to work towards this goal, and we
-welcome contributions to the library about any topic in mathematics.
+created by [Elisabeth Stenholm](https://elisabeth.bonnevier.one), Jonathan
+Prieto-Cubides, and [Egbert Rijke](https://egbertrijke.github.io), and is
+currently being maintained by Egbert Rijke,
+[Fredrik Bakke](https://www.ntnu.edu/employees/fredrik.bakke), and
+[Vojtěch Štěpančík](https://vojtechstep.eu/). Our goal is to formalize an
+extensive curriculum of mathematics from the univalent point of view.
+Furthermore, we think libraries of formalized mathematics have the potential to
+be useful, and informative resources for mathematicians. Our library is designed
+to work towards this goal, and we welcome contributions to the library about any
+topic in mathematics.
 
 ## Links
 

diff --git a/VISUALIZATION.md b/VISUALIZATION.md
@@ -28,9 +28,11 @@ allows you to determine dependencies between individual definitions. Hover over
   </iframe>
 </div>
 
-The interactive explorer was developed by Job Petrovčič. In addition, Vojtěch
-Štěpančík, Matej Petković, and Andrej Bauer contributed invaluable suggestions
-and offered helpful support.
+The interactive explorer was developed by
+[Job Petrovčič](https://github.com/JobPetrovcic). In addition,
+[Vojtěch Štěpančík](https://vojtechstep.eu/), Matej Petković, and
+[Andrej Bauer](https://www.andrej.com) contributed invaluable suggestions and
+offered helpful support.
 
 ### Notes
 

diff --git a/src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md b/src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md
@@ -39,7 +39,8 @@ The **binomial theorem** in commutative rings asserts that for any two elements
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
-The binomial theorem is the 44th theorem on Freek Wiedijk's list of
+The binomial theorem is the 44th theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) 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
@@ -39,7 +39,8 @@ we have
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
-The binomial theorem is the 44th theorem on Freek Wiedijk's list of
+The binomial theorem is the 44th theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) 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
@@ -38,9 +38,10 @@ open import foundation.unit-type
 
 </details>
 
-Bézout's Lemma is the 60th theorem on Freek Wiedijk's list of
+Bézout's Lemma is the 60th theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}. It was
-originally added to agda-unimath by [Brian Lu](https://blu-bird.github.io).
+originally added to agda-unimath by [Bryan Lu](https://blu-bird.github.io).
 
 ## Lemma
 

diff --git a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md b/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md
@@ -61,9 +61,10 @@ predicate `P : ℕ → UU lzero` given by
 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 list of
+Bézout's Lemma is the 60th theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}. It was
-originally added to agda-unimath by [Brian Lu](https://blu-bird.github.io).
+originally added to agda-unimath by [Bryan Lu](https://blu-bird.github.io).
 
 ## Definitions
 

diff --git a/src/elementary-number-theory/binomial-theorem-integers.lagda.md b/src/elementary-number-theory/binomial-theorem-integers.lagda.md
@@ -36,7 +36,8 @@ The binomial theorem for the integers asserts that for any two integers `x` and
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
-The binomial theorem is the 44th theorem on Freek Wiedijk's list of
+The binomial theorem is the 44th theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) 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
@@ -35,7 +35,8 @@ numbers `x` and `y` and any natural number `n`, we have
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
-The binomial theorem is the 44th theorem on Freek Wiedijk's list of
+The binomial theorem is the 44th theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) 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
@@ -75,8 +75,9 @@ in several ways:
 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
-list of [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+The fundamental theorem of arithmetic is the 80th theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions
 

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

diff --git a/src/foundation/cantor-schroder-bernstein-escardo.lagda.md b/src/foundation/cantor-schroder-bernstein-escardo.lagda.md
@@ -38,8 +38,9 @@ Escardó proved that a Cantor–Schröder–Bernstein theorem also holds for
 [embed](foundation-core.embeddings.md) into each other, then the types are
 [equivalent](foundation-core.equivalences.md). {{#cite Esc21}}
 
-The Cantor–Schröder–Bernstein theorem is the 25th theorem on Freek Wiedijk's
-list of [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+The Cantor–Schröder–Bernstein theorem is the 25th theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) 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
@@ -57,7 +57,8 @@ 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 list of
+Cantor's theorem is the 63rd theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ```agda

diff --git a/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md b/src/foundation/regensburg-extension-fundamental-theorem-of-identity-types.lagda.md
@@ -76,8 +76,9 @@ this condition is equivalent to the condition that `Σ A B` is `P`-separated.
 
 This theorem was stated and proven for the first time during the
 [Interactions of Proof Assistants and Mathematics](https://itp-school-2023.github.io)
-summer school in Regensburg, 2023, as part of Egbert Rijke's tutorial on
-formalization in agda-unimath.
+summer school in Regensburg, 2023, as part of
+[Egbert Rijke](https://egbertrijke.github.io)'s tutorial on formalization in
+agda-unimath.
 
 ## Theorem
 

diff --git a/src/literature/100-theorems.lagda.md b/src/literature/100-theorems.lagda.md
@@ -1,6 +1,7 @@
 # Formalizing 100 Theorems
 
-This file records formalized results from Freek Wiedijk's
+This file records formalized results from
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/)
 [_Formalizing 100 Theorems_](https://www.cs.ru.nl/~freek/100/).
 {{#cite 100theorems}}
 
@@ -12,7 +13,7 @@ module literature.100-theorems where
 
 ### [3. The Denumerability of the Rational Numbers](https://www.cs.ru.nl/~freek/100/#3) {#3}
 
-Author: Fredrik Bakke
+**Author:** [Fredrik Bakke](https://www.ntnu.edu/employees/fredrik.bakke)
 
 ```agda
 open import elementary-number-theory.rational-numbers using
@@ -21,7 +22,7 @@ open import elementary-number-theory.rational-numbers using
 
 ### [11. The Infinitude of Primes](https://www.cs.ru.nl/~freek/100/#11) {#11}
 
-Author: Egbert Rijke
+**Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
 ```agda
 open import elementary-number-theory.infinitude-of-primes using
@@ -34,7 +35,7 @@ open import elementary-number-theory.infinitude-of-primes using
 
 ### [25. Schröder–Bernstein Theorem](https://www.cs.ru.nl/~freek/100/#25) {#25}
 
-Author: Elif Uskuplu
+**Author:** [Elif Uskuplu](https://elifuskuplu.github.io)
 
 Note: The formalization of the Cantor-Schröder-Bernstein theorem in agda-unimath
 is a generalization of the statement to all types, i.e., it is not restricted to
@@ -50,7 +51,7 @@ open import foundation.cantor-schroder-bernstein-escardo using
 
 ### [44. The Binomial Theorem](https://www.cs.ru.nl/~freek/100/#44) {#44}
 
-Author: Egbert Rijke
+**Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
 ```agda
 open import commutative-algebra.binomial-theorem-commutative-rings using
@@ -69,7 +70,7 @@ open import elementary-number-theory.binomial-theorem-natural-numbers using
 
 ### [52. The Number of Subsets of a Set](https://www.cs.ru.nl/~freek/100/#52) {#52}
 
-Author: Egbert Rijke
+**Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
 ```agda
 open import univalent-combinatorics.decidable-subtypes using
@@ -78,7 +79,7 @@ open import univalent-combinatorics.decidable-subtypes using
 
 ### [58. Formula for the number of combinations](https://www.cs.ru.nl/~freek/100/#58) {#58}
 
-Author: Egbert Rijke
+**Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
 ```agda
 open import univalent-combinatorics.binomial-types using
@@ -87,7 +88,7 @@ open import univalent-combinatorics.binomial-types using
 
 ### [60. Bezout's Lemma](https://www.cs.ru.nl/~freek/100/#60) {#60}
 
-Author: Brian Lu
+**Author:** [Bryan Lu](https://blu-bird.github.io)
 
 Note that the 60th theorem in Freek's list is listed as "Bezout's Theorem",
 while the linked theorems are formalizations of Bezout's lemma, even though
@@ -102,7 +103,7 @@ open import elementary-number-theory.bezouts-lemma-natural-numbers using
 
 ### [63. Cantor's Theorem](https://www.cs.ru.nl/~freek/100/#63) {#63}
 
-Author: Egbert Rijke
+**Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
 ```agda
 open import foundation.cantors-theorem using
@@ -111,7 +112,7 @@ open import foundation.cantors-theorem using
 
 ### [69. Greatest Common Divisor Algorithm](https://www.cs.ru.nl/~freek/100/#69) {#69}
 
-Author: Egbert Rijke
+**Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
 ```agda
 open import
@@ -121,7 +122,7 @@ open import
 
 ### [74. The Principle of Mathematical Induction](https://www.cs.ru.nl/~freek/100/#74) {#74}
 
-Author: Egbert Rijke
+**Author:** [Egbert Rijke](https://egbertrijke.github.io)
 
 ```agda
 open import elementary-number-theory.natural-numbers using
@@ -130,7 +131,7 @@ open import elementary-number-theory.natural-numbers using
 
 ### [80. The Fundamental Theorem of Arithmetic](https://www.cs.ru.nl/~freek/100/#80) {#80}
 
-Author: Victor Blanchi
+**Author:** [Victor Blanchi](https://github.com/VictorBlanchi)
 
 ```agda
 open import elementary-number-theory.fundamental-theorem-of-arithmetic using
@@ -139,7 +140,7 @@ open import elementary-number-theory.fundamental-theorem-of-arithmetic using
 
 ### [91. The Triangle Inequality](https://www.cs.ru.nl/~freek/100/#91) {#91}
 
-Author: malarbol
+**Author:** [malarbol](https://github.com/malarbol)
 
 ```agda
 open import real-numbers.metric-space-of-real-numbers using

diff --git a/src/real-numbers/metric-space-of-real-numbers.lagda.md b/src/real-numbers/metric-space-of-real-numbers.lagda.md
@@ -98,7 +98,8 @@ 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 list of
+The triangle inequality is the 91st theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) 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
@@ -38,7 +38,8 @@ have
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
-The binomial theorem is the 44th theorem on Freek Wiedijk's list of
+The binomial theorem is the 44th theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) 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
@@ -41,7 +41,8 @@ have
   (x + y)ⁿ = ∑_{0 ≤ i < n+1} (n choose i) xⁱ yⁿ⁻ⁱ.
 ```
 
-The binomial theorem is the 44th theorem on Freek Wiedijk's list of
+The binomial theorem is the 44th theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ## Definitions

diff --git a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
@@ -791,4 +791,5 @@ module _
 - [Eckmann-Hilton argument](https://en.wikipedia.org/wiki/Eckmann%E2%80%93Hilton_argument)
   at Wikipedia
 - [Eckmann-Hilton and the Hopf Fibration](https://www.youtube.com/watch?v=hU4_dVpmkKM)
-  recorded talk given by Raymond Baker at HoTT-UF 24
+  recorded talk given by [Raymond Baker](https://morphismz.github.io) at HoTT-UF
+  24
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 list of
+is the 58th theorem on [Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
 [100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ```agda