name links

UniMath · Oct 29, 2024 · abdbd19 · abdbd19
1 parent 6b1eea6
commit abdbd19
Show file tree

Hide file tree

Showing 5 changed files with 15 additions and 15 deletions.
diff --git a/README.md b/README.md
@@ -2,11 +2,11 @@
 
 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](https://elisabeth.stenholm.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
+created by [Elisabeth Stenholm](https://elisabeth.stenholm.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 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

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
@@ -42,9 +42,9 @@ The greatest common divisor of two natural numbers `x` and `y` is a number
 `gcd x y` such that any natural number `d : ℕ` is a common divisor of `x` and
 `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 list of [100 theorems](literature.100-theorems.md)
-{{#cite 100theorems}}.
+The algorithm defining the greatest common divisor is the 69th 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/elementary-number-theory/natural-numbers.lagda.md b/src/elementary-number-theory/natural-numbers.lagda.md
@@ -83,9 +83,9 @@ 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 list of [100 theorems](literature.100-theorems.md)
-{{#cite 100theorems}}.
+The induction principle of the natural numbers is the 74th theorem on
+[Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/) list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
 
 ```agda
 ind-ℕ :

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

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
@@ -60,7 +60,7 @@ Labeled-Finite-Directed-Graph = Σ ℕ (λ n → Fin n → Fin n → ℕ)
 
 - [Digraph](https://ncatlab.org/nlab/show/digraph) at $n$Lab
 - [Directed graph](https://ncatlab.org/nlab/show/directed+graph) at $n$Lab
-- [Directed graph](https://www.wikidata.org/entity/Q1137726) on Wikdiata
+- [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