chore: some fixes to links

CONTRIBUTORS.toml

@@ -35,7 +35,7 @@ in Trondheim. His research is on homotopy type theory and higher category theory
 displayName = "Elisabeth Stenholm"
 maintainer = true
 usernames = [ "Elisabeth Stenholm", "Elisabeth Bonnevier" ]
-homepage = "https://elisabeth.bonnevier.one"
+homepage = "https://elisabeth.stenholm.one"
 github = "elisabethstenholm"
 bio = '''
 Elisabeth is a PhD student at the University of Bergen. Her research is on

HOME.md

@@ -9,7 +9,7 @@ typed programming language [Agda](https://github.com/agda/agda).
 </a>
 
 The library project was created by
-[Elisabeth Stenholm](https://elisabeth.bonnevier.one),
+[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),

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.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
+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

references.bib

@@ -508,6 +508,7 @@ @online{oeis
   title        = {The {{On-Line Encyclopedia}} of {{Integer Sequences}}},
   author       = {OEIS Foundation Inc.},
   date         = {1996},
+  citeas       = {OEIS},
   url          = {https://oeis.org},
   howpublished = {website},
 }

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
 

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-ℕ :

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

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

src/literature/100-theorems.lagda.md

@@ -1,4 +1,4 @@
-# Formalizing 100 Theorems
+# Freek Wiedijk's 100 Theorems
 
 This file records formalized results from
 [Freek Wiedijk's](http://www.cs.ru.nl/F.Wiedijk/)