diff --git a/src/graph-theory/acyclic-undirected-graphs.lagda.md b/src/graph-theory/acyclic-undirected-graphs.lagda.md
index caca26aa95..e2e083b6dd 100644
--- a/src/graph-theory/acyclic-undirected-graphs.lagda.md
+++ b/src/graph-theory/acyclic-undirected-graphs.lagda.md
@@ -18,21 +18,24 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-An **acyclic** undirected graph is an undirected graph of which the geometric
-realization is contractible.
+An **acyclic undirected graph** is an
+[undirected graph](graph-theory.undirected-graphs.md) of which the
+[geometric realization](graph-theory.geometric-realizations-undirected-graphs.md)
+is [contractible](foundation-core.contractible-types.md).
 
 The notion of acyclic graphs is a generalization of the notion of
 [undirected trees](trees.undirected-trees.md). Note that in this library, an
-undirected tree is an undirected graph in which the type of trails between any
-two points is contractible. The type of nodes of such undirected trees
-consequently has decidable equality. On the other hand, there are acyclic
-undirected graphs that are not undirected trees in this sense. One way to obtain
-them is via [acyclic types](synthetic-homotopy-theory.acyclic-types.md), which
-are types of which the
-[suspension](synthetic-homotopy-theory.suspensions-of-types.md) is contractible.
-The undirected suspension diagram of such types is an acyclic graph.
-Furthermore, any [directed tree](trees.directed-trees.md) induces an acyclic
-undirected graph by forgetting the directions of the edges.
+undirected tree is an undirected graph in which the type of
+[trails](graph-theory.trails-undirected-graphs.md) between any two points is
+contractible. The type of nodes of such undirected trees consequently has
+[decidable equality](foundation.decidable-equality.md). On the other hand, there
+are acyclic undirected graphs that are not undirected trees in this sense. One
+way to obtain them is via
+[acyclic types](synthetic-homotopy-theory.acyclic-types.md), which are types of
+which the [suspension](synthetic-homotopy-theory.suspensions-of-types.md) is
+contractible. The undirected suspension diagram of such types is an acyclic
+graph. Furthermore, any [directed tree](trees.directed-trees.md) induces an
+acyclic undirected graph by forgetting the directions of the edges.
 
 ## Definition
 
@@ -57,3 +60,12 @@ is-acyclic-Undirected-Graph l G =
 ### Table of files related to cyclic types, groups, and rings
 
 {{#include tables/cyclic-types.md}}
+
+## External links
+
+- [Trees](https://ncatlab.org/nlab/show/tree) at nlab
+- [Acyclic graph](https://www.wikidata.org/wiki/Q3115453) at Wikidata
+- [Forests](<https://en.wikipedia.org/wiki/Tree_(graph_theory)#Forest>) at
+  Wikipedia
+- [Acyclic graphs](https://mathworld.wolfram.com/AcyclicGraph.html) at Wolfram
+  Mathworld.
diff --git a/src/graph-theory/circuits-undirected-graphs.lagda.md b/src/graph-theory/circuits-undirected-graphs.lagda.md
index 98a01db985..76f293c10e 100644
--- a/src/graph-theory/circuits-undirected-graphs.lagda.md
+++ b/src/graph-theory/circuits-undirected-graphs.lagda.md
@@ -21,9 +21,12 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-A circuit in an undirected graph `G` consists of a `k`-gon `H` equipped with a
-totally faithful morphism of graphs from `H` to `G`. In other words, a circuit
-is a closed walk with no repeated edges.
+A **circuit** in an [undirected graph](graph-theory.undirected-graphs.md) `G`
+consists of a [`k`-gon](graph-theory.polygons.md) `H` equipped with a
+[totally faithful](graph-theory.totally-faithful-morphisms-undirected-graphs.md)
+[morphism](graph-theory.morphisms-undirected-graphs.md) of undirected graphs
+from `H` to `G`. In other words, a circuit is a closed walk with no repeated
+edges.
 
 ## Definition
 
@@ -38,3 +41,11 @@ module _
       ( λ H →
         totally-faithful-hom-Undirected-Graph (undirected-graph-Polygon k H) G)
 ```
+
+## External links
+
+- [Cycle](https://www.wikidata.org/wiki/Q245595) at Wikidata
+- [Cycle (Graph Theory)](<https://en.wikipedia.org/wiki/Cycle_(graph_theory)>)
+  at Wikipedia
+- [Graph Cycle](https://mathworld.wolfram.com/GraphCycle.html) at Wolfram
+  Mathworld
diff --git a/src/graph-theory/closed-walks-undirected-graphs.lagda.md b/src/graph-theory/closed-walks-undirected-graphs.lagda.md
index d804af430c..d104796216 100644
--- a/src/graph-theory/closed-walks-undirected-graphs.lagda.md
+++ b/src/graph-theory/closed-walks-undirected-graphs.lagda.md
@@ -21,8 +21,10 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-A closed walk of length `k : ℕ` in an undirected graph `G` is a morphism of
-graphs from a `k`-gon into `G`.
+A **closed walk** of length `k : ℕ` in an
+[undirected graph](graph-theory.undirected-graphs.md) `G` is a
+[morphism](graph-theory.morphisms-undirected-graphs.md) of graphs from a
+[`k`-gon](graph-theory.polygons.md) into `G`.
 
 ## Definition
 
@@ -35,3 +37,11 @@ module _
   closed-walk-Undirected-Graph =
     Σ (Polygon k) (λ H → hom-Undirected-Graph (undirected-graph-Polygon k H) G)
 ```
+
+## External links
+
+- [Cycle](https://www.wikidata.org/wiki/Q245595) at Wikidata
+- [Cycle (Graph Theory)](<https://en.wikipedia.org/wiki/Cycle_(graph_theory)>)
+  at Wikipedia
+- [Graph Cycle](https://mathworld.wolfram.com/GraphCycle.html) at Wolfram
+  Mathworld
diff --git a/src/graph-theory/complete-bipartite-graphs.lagda.md b/src/graph-theory/complete-bipartite-graphs.lagda.md
index 4c513cb1ab..8759afd50a 100644
--- a/src/graph-theory/complete-bipartite-graphs.lagda.md
+++ b/src/graph-theory/complete-bipartite-graphs.lagda.md
@@ -46,3 +46,14 @@ pr2 (complete-bipartite-Undirected-Graph-𝔽 X Y) p =
           ( element-unordered-pair p)
           ( inr y)))
 ```
+
+## External links
+
+- [Complete bipartite graph](https://d3gt.com/unit.html?complete-bipartite) at
+  D3 Graph Theory
+- [Bipartite graphs](https://ncatlab.org/nlab/show/bipartite+graph) at nlab
+- [Complete bipartite graph](https://www.wikidata.org/wiki/Q913598) at Wikidata
+- [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
diff --git a/src/graph-theory/complete-multipartite-graphs.lagda.md b/src/graph-theory/complete-multipartite-graphs.lagda.md
index bf6a9f671f..ed7d4a577e 100644
--- a/src/graph-theory/complete-multipartite-graphs.lagda.md
+++ b/src/graph-theory/complete-multipartite-graphs.lagda.md
@@ -24,9 +24,10 @@ open import univalent-combinatorics.function-types
 
 ## Idea
 
-A complete multipartite graph consists of a finite list of sets `V1,…,Vn`, and
-for each unordered pair of distinct elements `i,j≤n` and each `x : Vi` and
-`y : Vj` an edge between `x` and `y`.
+A **complete multipartite graph** consists of a [list](lists.lists.md) of sets
+`V1,…,Vn`, and for each [unordered pair](foundation.unordered-pairs.md) of
+distinct elements `i,j≤n` and each `x : Vi` and `y : Vj` an edge between `x` and
+`y`.
 
 ```agda
 complete-multipartite-Undirected-Graph-𝔽 :
@@ -43,3 +44,11 @@ pr2 (complete-multipartite-Undirected-Graph-𝔽 X Y) p =
                   ( pr1 (element-unordered-pair p y))))) →-𝔽
   empty-𝔽
 ```
+
+## External links
+
+- [Multipartite graph](https://www.wikidata.org/wiki/Q1718082) on Wikidata
+- [Multipartite graph](https://en.wikipedia.org/wiki/Multipartite_graph) on
+  Wikipedia
+- [Complete multipartite graph](https://mathworld.wolfram.com/CompleteMultipartiteGraph.html)
+  on Wolfram Mathworld
diff --git a/src/graph-theory/complete-undirected-graphs.lagda.md b/src/graph-theory/complete-undirected-graphs.lagda.md
index 0fa96550c6..a4f0a48d19 100644
--- a/src/graph-theory/complete-undirected-graphs.lagda.md
+++ b/src/graph-theory/complete-undirected-graphs.lagda.md
@@ -19,12 +19,15 @@ open import univalent-combinatorics.finite-types
 
 ## Idea
 
-A complete undirected graph is a complete multipartite graph in which every
-block has exactly one vertex. In other words, it is an undirected graph in which
-every vertex is connected to every other vertex.
+A **complete undirected graph** is a
+[complete multipartite graph](graph-theory.complete-multipartite-graphs.md) in
+which every block has exactly one vertex. In other words, it is an
+[undirected graph](graph-theory.undirected-graphs.md) in which every vertex is
+connected to every other vertex.
 
 There are many ways of presenting complete undirected graphs. For example, the
-type of edges in a complete undirected graph is a 2-element subtype of the type
+type of edges in a complete undirected graph is a
+[2-element subtype](univalent-combinatorics.2-element-subtypes.md) of the type
 of its vertices.
 
 ## Definition
@@ -34,3 +37,11 @@ complete-Undirected-Graph-𝔽 : {l : Level} → 𝔽 l → Undirected-Graph-
 complete-Undirected-Graph-𝔽 X =
   complete-multipartite-Undirected-Graph-𝔽 X (λ x → unit-𝔽)
 ```
+
+## External links
+
+- [Complete graph](https://d3gt.com/unit.html?complete-graph) at D3 Graph theory
+- [Complete graph](https://www.wikidata.org/wiki/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
diff --git a/src/graph-theory/connected-undirected-graphs.lagda.md b/src/graph-theory/connected-undirected-graphs.lagda.md
index f4f4a3da0c..9c6f3e0cd3 100644
--- a/src/graph-theory/connected-undirected-graphs.lagda.md
+++ b/src/graph-theory/connected-undirected-graphs.lagda.md
@@ -19,8 +19,9 @@ open import graph-theory.walks-undirected-graphs
 
 ## Idea
 
-A graph is said to be connected if any point can be reached from any point by a
-walk.
+An [undirected graph](graph-theory.undirected-graphs.md) is said to be
+**connected** if any point can be reached from any point by a
+[walk](graph-theory.walks-undirected-graphs.md).
 
 ## Definition
 
@@ -45,3 +46,12 @@ module _
   is-prop-is-connected-Undirected-Graph =
     is-prop-Π (λ _ → is-prop-Π (λ _ → is-prop-type-trunc-Prop))
 ```
+
+## External links
+
+- [Connected graph](https://ncatlab.org/nlab/show/connected+graph) at nlab
+- [Connected graph](https://www.wikidata.org/wiki/Q230655) on Wikidata
+- [Connectivity (graph theory)](<https://en.wikipedia.org/wiki/Connectivity_(graph_theory)>)
+  on Wikipedia
+- [Connected graph](https://mathworld.wolfram.com/ConnectedGraph.html) at
+  Wolfram Mathworld
diff --git a/src/graph-theory/cycles-undirected-graphs.lagda.md b/src/graph-theory/cycles-undirected-graphs.lagda.md
index bc41fe9830..30c80fdabd 100644
--- a/src/graph-theory/cycles-undirected-graphs.lagda.md
+++ b/src/graph-theory/cycles-undirected-graphs.lagda.md
@@ -21,8 +21,10 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-A cycle in an undirected graph `G` consists of a `k`-gon `H` equipped with an
-embedding of graphs from `H` into `G`.
+A **cycle** in an [undirected graph](graph-theory.undirected-graphs.md) `G`
+consists of a [`k`-gon](graph-theory.polygons.md) `H` equipped with an
+[embedding of graphs](graph-theory.embeddings-undirected-graphs.md) from `H`
+into `G`.
 
 ## Definition
 
@@ -35,3 +37,11 @@ module _
   cycle-Undirected-Graph =
     Σ (Polygon k) (λ H → emb-Undirected-Graph (undirected-graph-Polygon k H) G)
 ```
+
+## External links
+
+- [Cycle](https://www.wikidata.org/wiki/Q245595) on Wikidata
+- [Cycle (graph theory)](<https://en.wikipedia.org/wiki/Cycle_(graph_theory)>)
+  at Wikipedia
+- [Graph cycle](https://mathworld.wolfram.com/GraphCycle.html) at Wolfram
+  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 e3edee82f2..075e78c1cf 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
@@ -23,3 +23,12 @@ open import univalent-combinatorics.standard-finite-types
 Directed-Graph-Fin : UU lzero
 Directed-Graph-Fin = Σ ℕ (λ V → Fin V → Fin V → ℕ)
 ```
+
+## External links
+
+- [Digraph](https://ncatlab.org/nlab/show/digraph) at nlab
+- [Directed graph](https://ncatlab.org/nlab/show/directed+graph) at nlab
+- [Directed graph](https://www.wikidata.org/wiki/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
diff --git a/src/graph-theory/directed-graphs.lagda.md b/src/graph-theory/directed-graphs.lagda.md
index e75e6571d2..6e2df76a48 100644
--- a/src/graph-theory/directed-graphs.lagda.md
+++ b/src/graph-theory/directed-graphs.lagda.md
@@ -23,10 +23,12 @@ valued relation of edges. Alternatively, one can define a directed graph to
 consist of a type `V` of **vertices**, a type `E` of **edges**, and a map
 `E → V × V` determining the **source** and **target** of each edge.
 
-To see that these two definitions are equivalent, recall that $\Sigma$-types
-preserve equivalences and a type family $A \to U$ is equivalent to
-$\sum_{(C : U)} C \to A$ by [type duality](foundation.type-duality.md). Using
-these two observations we make the following calculation:
+To see that these two definitions are
+[equivalent](foundation-core.equivalences.md), recall that
+[$\Sigma$-types](foundation.dependent-pair-types.md) preserve equivalences and a
+type family $A \to U$ is equivalent to $\sum_{(C : U)} C \to A$ by
+[type duality](foundation.type-duality.md). Using these two observations we make
+the following calculation:
 
 $$
 \begin{equation}
@@ -130,3 +132,12 @@ module equiv {l1 l2 : Level} where
   pr2 (Directed-Graph'-to-Directed-Graph (V , E , st , tg)) x y =
     Σ E (λ e → (Id (st e) x) × (Id (tg e) y))
 ```
+
+## External links
+
+- [Digraph](https://ncatlab.org/nlab/show/digraph) at nlab
+- [Directed graph](https://ncatlab.org/nlab/show/directed+graph) at nlab
+- [Directed graph](https://www.wikidata.org/wiki/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
diff --git a/src/graph-theory/edge-coloured-undirected-graphs.lagda.md b/src/graph-theory/edge-coloured-undirected-graphs.lagda.md
index 77a4da00bd..2e7dadf0ef 100644
--- a/src/graph-theory/edge-coloured-undirected-graphs.lagda.md
+++ b/src/graph-theory/edge-coloured-undirected-graphs.lagda.md
@@ -20,10 +20,12 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-An edge-coloured undirected graph is an undirected graph equipped with a family
-of maps `E p → X` from the edges at unordered pairs `p` into a type `C` of
-colours, such that the induced map `incident-Undirected-Graph G x → C` is
-injective for each vertex `x`.
+An **edge-coloured undirected graph** is an
+[undirected graph](graph-theory.undirected-graphs.md) equipped with a family of
+maps `E p → X` from the edges at
+[unordered pairs](foundation.unordered-pairs.md) `p` into a type `C` of colours,
+such that the induced map `incident-Undirected-Graph G x → C` is
+[injective](foundation.injective-maps.md) for each vertex `x`.
 
 ## Definition
 
@@ -99,3 +101,10 @@ module _
   is-emb-colouring-Edge-Coloured-Undirected-Graph =
     pr2 (pr2 G)
 ```
+
+## External links
+
+- [Edge coloring](https://en.wikipedia.org/wiki/Edge_coloring) at Wikipedia
+- [Edge coloring](https://mathworld.wolfram.com/EdgeColoring.html) at Wolfram
+  Mathworld
+- [Graph coloring](https://www.wikidata.org/wiki/Q504843) on Wikidata
diff --git a/src/graph-theory/embeddings-directed-graphs.lagda.md b/src/graph-theory/embeddings-directed-graphs.lagda.md
index d280439f96..38b1099f19 100644
--- a/src/graph-theory/embeddings-directed-graphs.lagda.md
+++ b/src/graph-theory/embeddings-directed-graphs.lagda.md
@@ -20,9 +20,11 @@ open import graph-theory.morphisms-directed-graphs
 
 ## Idea
 
-An embedding of directed graphs is a morphism `f : G → H` of directed graphs
-which is an embedding on vertices such that for each pair `(x , y)` of vertices
-in `G` the map
+An **embedding of directed graphs** is a
+[morphism](graph-theory.morphisms-directed-graphs.md) `f : G → H` of
+[directed graphs](graph-theory.directed-graphs.md) which is an
+[embedding](foundation.embeddings.md) on vertices such that for each pair
+`(x , y)` of vertices in `G` the map
 
 ```text
   edge-hom-Graph G H : edge-Graph G p → edge-Graph H x y
@@ -31,6 +33,10 @@ in `G` the map
 is also an embedding. Embeddings of directed graphs correspond to directed
 subgraphs.
 
+**Note:** Our notion of embeddings of directed graphs differs quite
+substantially from the graph theoretic notion of _graph embedding_, which
+usually refers to an embedding of a graph into the plane.
+
 ## Definition
 
 ```agda
@@ -64,3 +70,9 @@ module _
     is-emb-hom-Directed-Graph (hom-emb-Directed-Graph f)
   is-emb-emb-Directed-Graph = pr2
 ```
+
+## External links
+
+- [Graph homomorphism](https://www.wikidata.org/wiki/Q3385162) on Wikidata
+- [Graph homomorphism](https://en.wikipedia.org/wiki/Graph_homomorphism) on
+  Wikipedia
diff --git a/src/graph-theory/embeddings-undirected-graphs.lagda.md b/src/graph-theory/embeddings-undirected-graphs.lagda.md
index 328b1256e4..c143ada208 100644
--- a/src/graph-theory/embeddings-undirected-graphs.lagda.md
+++ b/src/graph-theory/embeddings-undirected-graphs.lagda.md
@@ -20,9 +20,11 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-An embedding of undirected graphs is a morphism `f : G → H` of undirected graphs
-which is an embedding on vertices such that for each unordered pair `p` of
-vertices in `G` the map
+An **embedding of undirected graphs** is a
+[morphism](graph-theory.morphisms-undirected-graphs.md) `f : G → H` of
+[undirected graphs](graph-theory.undirected-graphs.md) which is an
+[embedding](foundation.embeddings.md) on vertices such that for each
+[unordered pair](foundation.unordered-pairs.md) `p` of vertices in `G` the map
 
 ```text
   edge-hom-Undirected-Graph G H :
@@ -33,6 +35,10 @@ vertices in `G` the map
 is also an embedding. Embeddings of undirected graphs correspond to undirected
 subgraphs.
 
+**Note:** Our notion of embeddings of directed graphs differs quite
+substantially from the graph theoretic notion of _graph embedding_, which
+usually refers to an embedding of a graph into the plane.
+
 ## Definition
 
 ```agda
@@ -119,5 +125,11 @@ module _
 
 ## See also
 
-- Faithful morphisms of undirected graphs
-- Totally faithful morphisms of undirected graphs
+- [Faithful morphisms of undirected graphs](graph-theory.faithful-morphisms-undirected-graphs.md)
+- [Totally faithful morphisms of undirected graphs](graph-theory.totally-faithful-morphisms-undirected-graphs.md)
+
+## External links
+
+- [Graph homomorphism](https://www.wikidata.org/wiki/Q3385162) on Wikidata
+- [Graph homomorphism](https://en.wikipedia.org/wiki/Graph_homomorphism) on
+  Wikipedia
diff --git a/src/graph-theory/enriched-undirected-graphs.lagda.md b/src/graph-theory/enriched-undirected-graphs.lagda.md
index 244f61ae60..5be1c2aaad 100644
--- a/src/graph-theory/enriched-undirected-graphs.lagda.md
+++ b/src/graph-theory/enriched-undirected-graphs.lagda.md
@@ -28,16 +28,20 @@ open import higher-group-theory.higher-groups
 ## Idea
 
 Consider a type `A` equipped with a type family `B` over `A`. An
-**`(A,B)`-enriched undirected graph** is an undirected graph `G := (V,E)`
-equipped with a map `sh : V → A`, and for each vertex `v` an equivalence from
-`B (sh v)` to the type of all edges going out of `v`, i.e., to the type
+**`(A,B)`-enriched undirected graph** is an
+[undirected graph](graph-theory.undirected-graphs.md) `G := (V,E)` equipped with
+a map `sh : V → A`, and for each vertex `v` an
+[equivalence](foundation-core.equivalences.md) from `B (sh v)` to the type of
+all edges going out of `v`, i.e., to the type `neighbor v` of
+[neighbors](graph-theory.neighbors-undirected-graphs.md).
+
+The map `sh : V → A` assigns to each vertex a shape, and with it an
+[∞-group](higher-group-theory.higher-groups.md) `BAut (sh v)`. The type family
+`B` restricted to `BAut (sh v)` is an
+[`Aut (sh v)`-type](higher-group-theory.higher-group-actions.md), and the
+equivalence `B (sh v) ≃ neighbor v` then ensures type type being acted on is
 `neighbor v`.
 
-The map `sh : V → A` assigns to each vertex a shape, and with it an ∞-group
-`BAut (sh v)`. The type family `B` restricted to `BAut (sh v)` is an
-`Aut (sh v)`-type, and the equivalence `B (sh v) ≃ neighbor v` then ensures type
-type being acted on is `neighbor v`.
-
 ## Definition
 
 ```agda
@@ -191,3 +195,11 @@ module _
                 ( action-∞-group-vertex-Enriched-Undirected-Graph v) h
                 ( map-inv-equiv-neighbor-Enriched-Undirected-Graph v x))))))
 ```
+
+## External links
+
+- [Graph](https://ncatlab.org/nlab/show/graph) at nlab
+- [Graph](https://www.wikidata.org/wiki/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
diff --git a/src/graph-theory/equivalences-directed-graphs.lagda.md b/src/graph-theory/equivalences-directed-graphs.lagda.md
index 05c41fbbaf..4e79106f79 100644
--- a/src/graph-theory/equivalences-directed-graphs.lagda.md
+++ b/src/graph-theory/equivalences-directed-graphs.lagda.md
@@ -34,6 +34,14 @@ open import graph-theory.morphisms-directed-graphs
 
 </details>
 
+## Idea
+
+An **equivalence of directed graphs** from a
+[directed graph](graph-theory.directed-graphs.md) `(V,E)` to a directed graph
+`(V',E')` consists of an [equivalence](foundation-core.equivalences.md)
+`e : V ≃ V'` of vertices, and a family of equivalences `E x y ≃ E' (e x) (e y)`
+of edges indexed by `x y : V`.
+
 ## Definitions
 
 ### Equivalences of directed graphs
@@ -530,3 +538,12 @@ module _
   pr2 is-retraction-inv-equiv-Directed-Graph =
     edge-is-retraction-inv-equiv-Directed-Graph
 ```
+
+## External links
+
+- [Graph isomoprhism](https://www.wikidata.org/wiki/Q303100) at Wikidata
+- [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
+  Wikipedia
+- [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
+  Wolfram Mathworld
+- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at nlab
diff --git a/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md b/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md
index 73ed13bcae..f479f770f9 100644
--- a/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md
+++ b/src/graph-theory/equivalences-enriched-undirected-graphs.lagda.md
@@ -30,9 +30,13 @@ open import graph-theory.neighbors-undirected-graphs
 
 ## Idea
 
-An equivalence of `(A,B)`-enriched undirected graphs from `G` to `H` consists of
-an equivalence `e` of the underlying graphs of `G` and `H` such that preserving
-the labeling and the equivalences on the neighbors
+An **equivalence of `(A,B)`-enriched undirected graphs** from an
+[`(A,B)`-enriched undirected graph](graph-theory.enriched-undirected-graphs.md)
+`G` to an `(A,B)`-enriched undirected graph `H` consists of an
+[equivalence](graph-theory.equivalences-undirected-graphs.md) `e` of the
+underlying graphs of `G` and `H` such that preserving the labeling and the
+[equivalences](foundation-core.equivalences.md) on the
+[neighbors](graph-theory.neighbors-undirected-graphs.md).
 
 ## Definition
 
@@ -293,3 +297,12 @@ module _
   eq-equiv-Enriched-Undirected-Graph H =
     map-inv-equiv (extensionality-Enriched-Undirected-Graph H)
 ```
+
+## External links
+
+- [Graph isomoprhism](https://www.wikidata.org/wiki/Q303100) at Wikidata
+- [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
+  Wikipedia
+- [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
+  Wolfram Mathworld
+- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at nlab
diff --git a/src/graph-theory/equivalences-undirected-graphs.lagda.md b/src/graph-theory/equivalences-undirected-graphs.lagda.md
index 8b5f0a65af..5b57e7da6f 100644
--- a/src/graph-theory/equivalences-undirected-graphs.lagda.md
+++ b/src/graph-theory/equivalences-undirected-graphs.lagda.md
@@ -33,8 +33,11 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-An equivalence of undirected graphs is a morphism of undirected graphs that
-induces an equivalence on vertices and equivalences on edges.
+An **equivalence of undirected graphs** is a
+[morphism](graph-theory.morphisms-undirected-graphs.md) of
+[undirected graphs](graph-theory.undirected-graphs.md) that induces an
+[equivalence](foundation-core.equivalences.md) on vertices and equivalences on
+edges.
 
 ## Definitions
 
@@ -294,3 +297,12 @@ module _
   eq-equiv-Undirected-Graph H =
     map-inv-is-equiv (is-equiv-equiv-eq-Undirected-Graph H)
 ```
+
+## External links
+
+- [Graph isomoprhism](https://www.wikidata.org/wiki/Q303100) at Wikidata
+- [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
+  Wikipedia
+- [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
+  Wolfram Mathworld
+- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at nlab
diff --git a/src/graph-theory/eulerian-circuits-undirected-graphs.lagda.md b/src/graph-theory/eulerian-circuits-undirected-graphs.lagda.md
index 1c9033d98d..8b08656a86 100644
--- a/src/graph-theory/eulerian-circuits-undirected-graphs.lagda.md
+++ b/src/graph-theory/eulerian-circuits-undirected-graphs.lagda.md
@@ -23,10 +23,13 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-An Eulerian cicuit in an undirected graph `G` consists of a cicuit `T` in `G`
-such that every edge in `G` is in the image of `T`. In other words, an Eulerian
-circuit `T` consists of `k`-gon `H` equipped with a graph homomorphism
-`f : H → G` that induces an equivalence
+An **Eulerian circuit** in an
+[undirected graph](graph-theory.undirected-graphs.md) `G` consists of a
+[circuit](graph-theory.circuits-undirected-graphs.md) `T` in `G` such that every
+edge in `G` is in the image of `T`. In other words, an Eulerian circuit `T`
+consists of [`k`-gon](graph-theory.polygons.md) `H` equipped with a
+[graph homomorphism](graph-theory.morphisms-undirected-graphs.md) `f : H → G`
+that induces an [equivalence](foundation-core.equivalences.md)
 
 ```text
   Σ (unordered-pair-vertices-Polygon k H) (edge-Polygon k H) ≃
@@ -55,3 +58,12 @@ module _
                       ( G)
                       ( f))))))
 ```
+
+## External links
+
+- [Eulerian circuit](https://d3gt.com/unit.html?eulerian-circuit) on D3 Graph
+  theory
+- [Eulerian cycle](https://www.wikidata.org/wiki/Q11691793) on Wikidata
+- [Eulerian path](https://en.wikipedia.org/wiki/Eulerian_path) on Wikipedia
+- [Eulerian cycle](https://mathworld.wolfram.com/EulerianCycle.html) on Wolfram
+  mathworld
diff --git a/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md b/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md
index 86daf7380d..0a0bbccc35 100644
--- a/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md
+++ b/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md
@@ -20,8 +20,10 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-A faithful morphism of undirected graphs is a morphism `f : G → H` of undirected
-graphs such that for each unordered pair `p` of vertices in `G` the map
+A **faithful morphism of undirected graphs** is a
+[morphism](graph-theory.morphisms-undirected-graphs.md) `f : G → H` of
+[undirected graphs](graph-theory.undirected-graphs.md) such that for each
+[unordered pair](foundation.unordered-pairs.md) `p` of vertices in `G` the map
 
 ```text
   edge-hom-Undirected-Graph G H f p :
@@ -30,7 +32,7 @@ graphs such that for each unordered pair `p` of vertices in `G` the map
       ( unordered-pair-vertices-hom-Undirected-Graph G H f p)
 ```
 
-is an embedding.
+is an [embedding](foundation.embeddings.md).
 
 ## Definition
 
@@ -114,5 +116,11 @@ module _
 
 ## See also
 
-- Embeddings of undirected graphs
-- Totally faithful morphisms of undirected graphs
+- [Embeddings of undirected graphs](graph-theory.embeddings-undirected-graphs.md)
+- [Totally faithful morphisms of undirected graphs](graph-theory.totally-faithful-morphisms-undirected-graphs.md)
+
+## External links
+
+- [Graph homomorphism](https://www.wikidata.org/wiki/Q3385162) on Wikidata
+- [Graph homomorphism](https://en.wikipedia.org/wiki/Graph_homomorphism) at
+  Wikipedia
diff --git a/src/graph-theory/fibers-directed-graphs.lagda.md b/src/graph-theory/fibers-directed-graphs.lagda.md
index 3b7917dec1..0c6d099217 100644
--- a/src/graph-theory/fibers-directed-graphs.lagda.md
+++ b/src/graph-theory/fibers-directed-graphs.lagda.md
@@ -29,10 +29,12 @@ open import trees.directed-trees
 
 ## Idea
 
-Consider a vertex `x` in a directed graph `G`. The fiber of `G` at `x` is a
-directed tree of which the type of nodes consists of vertices `y` equipped with
-a walk `w` from `y` to `x`, and the type of edges from `(y , w)` to `(z , v)`
-consist of an edge `e : y → z` such that `w ＝ cons e v`.
+Consider a vertex `x` in a [directed graph](graph-theory.directed-graphs.md)
+`G`. The **fiber** of `G` at `x` is a [directed tree](trees.directed-trees.md)
+of which the type of nodes consists of vertices `y` equipped with a
+[walk](graph-theory.walks-directed-graphs.md) `w` from `y` to `x`, and the type
+of edges from `(y , w)` to `(z , v)` consist of an edge `e : y → z` such that
+`w ＝ cons e v`.
 
 ## Definitions
 
diff --git a/src/graph-theory/finite-graphs.lagda.md b/src/graph-theory/finite-graphs.lagda.md
index 8491048184..61790646a7 100644
--- a/src/graph-theory/finite-graphs.lagda.md
+++ b/src/graph-theory/finite-graphs.lagda.md
@@ -24,8 +24,14 @@ open import univalent-combinatorics.finite-types
 
 ## Idea
 
-A finite undirected graph consists of a finite set of vertices and a family of
-finite types of edges indexed by unordered pairs of vertices.
+A **finite undirected graph** consists of a
+[finite set](univalent-combinatorics.finite-types.md) of vertices and a family
+of finite types of edges indexed by
+[unordered pairs](foundation.unordered-pairs.md) of vertices.
+
+**Note:** In our definition of finite graph, we allow for the possibility that
+there are multiple edges between the same two nodes. In discrete mathematics it
+is also common to call such graphs _multigraphs_.
 
 ## Definitions
 
@@ -93,3 +99,11 @@ incident-edges-vertex-Undirected-Graph-𝔽 G x =
   Σ ( unordered-pair (vertex-Undirected-Graph-𝔽 G))
     ( λ p → fiber (element-unordered-pair p) x)
 ```
+
+## External links
+
+- [Multigraph](https://ncatlab.org/nlab/show/multigraph) at nlab
+- [Multigraph](https://www.wikidata.org/wiki/Q2642629) on Wikidata
+- [Multigraph](https://en.wikipedia.org/wiki/Multigraph) at Wikipedia
+- [Multigraph](https://mathworld.wolfram.com/Multigraph.html) at Wolfram
+  mathworld
diff --git a/src/graph-theory/geometric-realizations-undirected-graphs.lagda.md b/src/graph-theory/geometric-realizations-undirected-graphs.lagda.md
index 220556ead9..69f6fd563d 100644
--- a/src/graph-theory/geometric-realizations-undirected-graphs.lagda.md
+++ b/src/graph-theory/geometric-realizations-undirected-graphs.lagda.md
@@ -21,8 +21,11 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-The geometric realization of an undirected graph `G` is the initial type `X`
-equipped with a reflecting map from `G` into `X`.
+The **geometric realization** of an
+[undirected graph](graph-theory.undirected-graphs.md) `G` is the initial type
+`X` equipped with a
+[reflecting map](graph-theory.reflecting-maps-undirected-graphs.md) from `G`
+into `X`.
 
 ## Definition
 
@@ -44,3 +47,8 @@ is-geometric-realization-reflecting-map-Undirected-Graph :
 is-geometric-realization-reflecting-map-Undirected-Graph l G f =
   (Y : UU l) → is-equiv (precomp-reflecting-map-Undirected-Graph G Y f)
 ```
+
+## External links
+
+- [Geometric realization](https://ncatlab.org/nlab/show/geometric+realization)
+  at nlab
diff --git a/src/graph-theory/hypergraphs.lagda.md b/src/graph-theory/hypergraphs.lagda.md
index 8bcc58817d..2081bbd9c1 100644
--- a/src/graph-theory/hypergraphs.lagda.md
+++ b/src/graph-theory/hypergraphs.lagda.md
@@ -18,8 +18,9 @@ open import foundation.unordered-tuples
 
 ## Idea
 
-A `k`-hypergraph consists of a type `V` of vertices and a family `E` of types
-indexed by the unordered `k`-tuples of vertices.
+A **`k`-hypergraph** consists of a type `V` of vertices and a family `E` of
+types indexed by the [unordered `k`-tuples](foundation.unordered-tuples.md) of
+vertices.
 
 ## Definition
 
@@ -40,3 +41,11 @@ module _
   simplex-Hypergraph : unordered-tuple-vertices-Hypergraph → UU l2
   simplex-Hypergraph = pr2 G
 ```
+
+## External links
+
+- [Hypergraph](https://ncatlab.org/nlab/show/hypergraph) at nlab
+- [Hypergraph](https://www.wikidata.org/wiki/Q840247) on Wikidata
+- [Hypergraph](https://en.wikipedia.org/wiki/Hypergraph) at Wikipedia
+- [Hypergraph](https://mathworld.wolfram.com/Hypergraph.html) at Wolfram
+  Mathworld
diff --git a/src/graph-theory/matchings.lagda.md b/src/graph-theory/matchings.lagda.md
index 3d12fe33a6..aeea1e538f 100644
--- a/src/graph-theory/matchings.lagda.md
+++ b/src/graph-theory/matchings.lagda.md
@@ -25,7 +25,8 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-A matching in a undirected graph is a set of edges without common vertices.
+A **matching** in a [undirected graph](graph-theory.undirected-graphs.md) is a
+type of edges without common vertices.
 
 ## Definitions
 
@@ -61,3 +62,10 @@ module _
         ( x : vertex-Undirected-Graph G) →
           is-contr (selected-edges-vertex-Undirected-Graph G c x))
 ```
+
+## External links
+
+- [Matching](https://www.wikidata.org/wiki/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
diff --git a/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md b/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md
index b5c8b2ab52..8fc2c50e10 100644
--- a/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md
+++ b/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md
@@ -19,8 +19,11 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-Two undirected graphs are said to be merely equivalent if there merely exists an
-equivalence of undirected graphs between them.
+Two [undirected graphs](graph-theory.undirected-graphs.md) are said to be
+**merely equivalent** if there merely
+[exists](foundation.existential-quantification.md) an
+[equivalence of undirected graphs](graph-theory.equivalences-undirected-graphs.md)
+between them.
 
 ## Definition
 
@@ -54,3 +57,12 @@ module _
   refl-mere-equiv-Undirected-Graph =
     unit-trunc-Prop (id-equiv-Undirected-Graph G)
 ```
+
+## External links
+
+- [Graph isomoprhism](https://www.wikidata.org/wiki/Q303100) at Wikidata
+- [Graph isomorphism](https://en.wikipedia.org/wiki/Graph_isomorphism) at
+  Wikipedia
+- [Graph isomorphism](https://mathworld.wolfram.com/GraphIsomorphism.html) at
+  Wolfram Mathworld
+- [Isomorphism](https://ncatlab.org/nlab/show/isomorphism) at nlab
diff --git a/src/graph-theory/morphisms-directed-graphs.lagda.md b/src/graph-theory/morphisms-directed-graphs.lagda.md
index 399e02bb27..19e6bbb57b 100644
--- a/src/graph-theory/morphisms-directed-graphs.lagda.md
+++ b/src/graph-theory/morphisms-directed-graphs.lagda.md
@@ -26,6 +26,12 @@ open import graph-theory.directed-graphs
 
 </details>
 
+## Idea
+
+A **morphism of directed graphs** from `G` to `H` consists of a map `f` from the
+vertices of `G` to the vertices of `H`, and a family of maps from the edges
+`E_G x y` in G`to the edges`E_H (f x) (f y)`in`H`.
+
 ## Definitions
 
 ### Morphisms of directed graphs
@@ -216,3 +222,9 @@ module _
   eq-htpy-hom-Directed-Graph f g =
     map-inv-equiv (extensionality-hom-Directed-Graph f g)
 ```
+
+## External links
+
+- [Graph homomorphism](https://www.wikidata.org/wiki/Q3385162) on Wikidata
+- [Graph homomorphism](https://en.wikipedia.org/wiki/Graph_homomorphism) at
+  Wikipedia
diff --git a/src/graph-theory/morphisms-undirected-graphs.lagda.md b/src/graph-theory/morphisms-undirected-graphs.lagda.md
index 6bae0d5ade..7fa3f0a986 100644
--- a/src/graph-theory/morphisms-undirected-graphs.lagda.md
+++ b/src/graph-theory/morphisms-undirected-graphs.lagda.md
@@ -195,3 +195,9 @@ module _
   eq-htpy-hom-Undirected-Graph f g =
     map-inv-is-equiv (is-equiv-htpy-eq-hom-Undirected-Graph f g)
 ```
+
+## External links
+
+- [Graph homomorphism](https://www.wikidata.org/wiki/Q3385162) on Wikidata
+- [Graph homomorphism](https://en.wikipedia.org/wiki/Graph_homomorphism) at
+  Wikipedia
diff --git a/src/graph-theory/neighbors-undirected-graphs.lagda.md b/src/graph-theory/neighbors-undirected-graphs.lagda.md
index 1131fd1d64..a3c2c7ee9f 100644
--- a/src/graph-theory/neighbors-undirected-graphs.lagda.md
+++ b/src/graph-theory/neighbors-undirected-graphs.lagda.md
@@ -80,3 +80,11 @@ neighbor-id-equiv-Undirected-Graph G x (pair y e) =
     ( refl)
     ( edge-standard-unordered-pair-vertices-id-equiv-Undirected-Graph G x y e)
 ```
+
+## External links
+
+- [Neighborhood](https://www.wikidata.org/wiki/Q1354987) on Wikidata
+- [Neighborhood (graph theory)](<https://en.wikipedia.org/wiki/Neighbourhood_(graph_theory)>)
+  at Wikipedia
+- [Graph neighborhood](https://mathworld.wolfram.com/GraphNeighborhood.html) at
+  Wolfram Mathworld
diff --git a/src/graph-theory/orientations-undirected-graphs.lagda.md b/src/graph-theory/orientations-undirected-graphs.lagda.md
index d2ef4925da..0b026ac4d4 100644
--- a/src/graph-theory/orientations-undirected-graphs.lagda.md
+++ b/src/graph-theory/orientations-undirected-graphs.lagda.md
@@ -41,3 +41,11 @@ module _
   source-edge-orientation-Undirected-Graph d (pair X p) e =
     p (d (pair X p) e)
 ```
+
+## External links
+
+- [Orientation](https://www.wikidata.org/wiki/Q7102401) on Wikidata
+- [Orientation (graph theory)](<https://en.wikipedia.org/wiki/Orientation_(graph_theory)>)
+  at Wikipedia
+- [Graph orientation](https://mathworld.wolfram.com/GraphOrientation.html) at
+  Wolfram Mathworld
diff --git a/src/graph-theory/paths-undirected-graphs.lagda.md b/src/graph-theory/paths-undirected-graphs.lagda.md
index 306c35fd92..cb2ca3206e 100644
--- a/src/graph-theory/paths-undirected-graphs.lagda.md
+++ b/src/graph-theory/paths-undirected-graphs.lagda.md
@@ -21,11 +21,17 @@ open import graph-theory.walks-undirected-graphs
 
 ## Idea
 
-A path in an undirected graph G is a walk `w` in G such that the inclusion of
-the type of vertices on `w` into the vertices of `G` is an injective function.
-Note that we don't expect this function to be an embedding, since the type of
-vertices on `w` is equivalent to `Fin (n + 1)` where `n` is the length of the
-walk, whereas the type of vertices of `G` does not need to be a set.
+A **path** in an [undirected graph](graph-theory.undirected-graphs.md) `G` is a
+[walk](graph-theory.walks-undirected-graphs.md) `w` in G such that the inclusion
+of the type of vertices on `w` into the vertices of `G` is an
+[injective](foundation.injective-maps.md) function.
+
+**Note:** It is too much to ask for for this function to be an
+[embedding](foundation-core.embeddings.md), since the type of vertices on `w` is
+equivalent to the
+[standard finite type](univalent-combinatorics.standard-finite-types.md)
+`Fin (n + 1)` where `n` is the length of the walk, whereas the type of vertices
+of `G` does not need to be a [set](foundation-core.sets.md).
 
 ## Definition
 
@@ -69,3 +75,11 @@ is-path-refl-walk-Undirected-Graph G x =
     ( vertex-vertex-on-walk-Undirected-Graph G refl-walk-Undirected-Graph)
     ( is-contr-vertex-on-walk-refl-walk-Undirected-Graph G x)
 ```
+
+## External links
+
+- [Path](https://www.wikidata.org/wiki/Q1415372) on Wikidata
+- [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
+  Wikipedia
+- [Graph path](https://mathworld.wolfram.com/GraphPath.html) at Wolfram
+  Mathworld
diff --git a/src/graph-theory/polygons.lagda.md b/src/graph-theory/polygons.lagda.md
index 9cd2058e1d..6083b49e78 100644
--- a/src/graph-theory/polygons.lagda.md
+++ b/src/graph-theory/polygons.lagda.md
@@ -30,10 +30,13 @@ open import univalent-combinatorics.finite-types
 
 ## Idea
 
-A polygon is an undirected graph that is merely equivalent to a graph with
-vertices `ℤ-Mod k` and an edge from each `x ∈ ℤ-Mod k` to `x+1`. This defines
-for each `k ∈ ℕ` the type of all `k`-gons. The type of all `k`-gons is a
-concrete presentation of the dihedral group `D_k`.
+A **polygon** is an [undirected graph](graph-theory.undirected-graphs.md) that
+is [merely equivalent](graph-theory.mere-equivalences-undirected-graphs.md) to a
+graph with vertices the underlying type of the
+[standard cyclic group](elementary-number-theory.standard-cyclic-groups.md)
+`ℤ-Mod k` and an edge from each `x ∈ ℤ-Mod k` to `x+1`. This defines for each
+`k ∈ ℕ` the type of all `k`-gons. The type of all `k`-gons is a concrete
+presentation of the [dihedral group](group-theory.dihedral-groups.md) `D_k`.
 
 ## Definition
 
@@ -115,12 +118,6 @@ module _
     has-decidable-equality-mere-equiv'
       ( mere-equiv-vertex-Polygon)
       ( has-decidable-equality-ℤ-Mod k)
-
-{-
-  is-prop-edge-Polygon :
-    (p : unordered-pair-vertices-Polygon) → is-prop (edge-Polygon p)
-  is-prop-edge-Polygon p = {!!}
--}
 ```
 
 ## Properties
@@ -135,44 +132,21 @@ is-set-vertex-standard-polygon-Undirected-Graph k = is-set-ℤ-Mod k
 
 ### Every edge is between distinct points
 
-```agda
-{-
-module _
-  (k : ℕ) (p : unordered-pair-vertices-standard-polygon-Undirected-Graph k)
-  where
-
-  is-emb-element-unordered-pair-edge-standard-polygon-Undirected-Graph :
-    edge-standard-polygon-Undirected-Graph k p →
-    is-emb (element-unordered-pair p)
-  is-emb-element-unordered-pair-edge-standard-polygon-Undirected-Graph e =
-    is-emb-is-injective
-      ( is-set-vertex-standard-polygon-Undirected-Graph k)
-      {!!}
-
-  is-prop-edge-standard-polygon-Undirected-Graph :
-    is-prop (edge-standard-polygon-Undirected-Graph k p)
-  is-prop-edge-standard-polygon-Undirected-Graph =
-    {!!}
--}
-```
+This remains to be formalized.
 
 ### Every polygon is a simple graph
 
-```agda
-{-
-is-simple-standard-polygon-Undirected-Graph :
-  (k : ℕ) → is-not-one-ℕ k →
-  is-simple-Undirected-Graph (standard-polygon-Undirected-Graph k)
-pr1 (is-simple-standard-polygon-Undirected-Graph k H) p (pair x (pair y α)) =
-  is-emb-is-injective
-    {!!}
-    {!!}
-pr2 (is-simple-standard-polygon-Undirected-Graph k H) p = {!!}
--}
-```
+This remains to be formalized.
 
 ## See also
 
 ### Table of files related to cyclic types, groups, and rings
 
 {{#include tables/cyclic-types.md}}
+
+## External links
+
+- [Cycle graph](https://www.wikidata.org/wiki/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
diff --git a/src/graph-theory/raising-universe-levels-directed-graphs.lagda.md b/src/graph-theory/raising-universe-levels-directed-graphs.lagda.md
index eef8033113..356c1b05be 100644
--- a/src/graph-theory/raising-universe-levels-directed-graphs.lagda.md
+++ b/src/graph-theory/raising-universe-levels-directed-graphs.lagda.md
@@ -21,8 +21,10 @@ open import graph-theory.walks-directed-graphs
 
 ## Idea
 
-We raise the universe levels of directed graphs by raising the universe levels
-of the vertices and the edges.
+We **raise the universe levels** of
+[directed graphs](graph-theory.directed-graphs.md) by
+[raising the universe levels](foundation.raising-universe-levels.md) of the
+vertices and the edges.
 
 ## Definition
 
diff --git a/src/graph-theory/reflecting-maps-undirected-graphs.lagda.md b/src/graph-theory/reflecting-maps-undirected-graphs.lagda.md
index 78212d3ae4..8f92c530a6 100644
--- a/src/graph-theory/reflecting-maps-undirected-graphs.lagda.md
+++ b/src/graph-theory/reflecting-maps-undirected-graphs.lagda.md
@@ -21,14 +21,16 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-A reflecting map from an undirected graph `(V , E)` into a type `X` consists of
-a map `fV : V → X` and a map
+A **reflecting map** from an
+[undirected graph](graph-theory.undirected-graphs.md) `(V , E)` into a type `X`
+consists of a map `fV : V → X` and a map
 
 ```text
   fE : (v : unordered-pair V) → E v → symmetric-Id (map-unordered-pair fV v).
 ```
 
-In other words, it maps edges into the symmetric identity type.
+In other words, it maps edges into the
+[symmetric identity type](foundation.symmetric-identity-types.md).
 
 ## Definitions
 
@@ -75,3 +77,8 @@ pr1 (pr2 (terminal-reflecting-map-Undirected-Graph G) p e) = star
 pr2 (pr2 (terminal-reflecting-map-Undirected-Graph G) p e) x =
   eq-is-contr is-contr-unit
 ```
+
+## External links
+
+- [Geometric realization](https://ncatlab.org/nlab/show/geometric+realization)
+  at nlab
diff --git a/src/graph-theory/reflexive-graphs.lagda.md b/src/graph-theory/reflexive-graphs.lagda.md
index d12da3d743..458fdcb536 100644
--- a/src/graph-theory/reflexive-graphs.lagda.md
+++ b/src/graph-theory/reflexive-graphs.lagda.md
@@ -15,7 +15,8 @@ open import foundation.universe-levels
 
 ## Idea
 
-A reflexive graph is a graph such that there is an loop edge at every vertex.
+A **reflexive graph** is a [directed graph](graph-theory.directed-graphs.md)
+such that there is an loop edge at every vertex.
 
 ## Definition
 
@@ -37,3 +38,11 @@ module _
   refl-Reflexive-Graph : (x : vertex-Reflexive-Graph) → edge-Reflexive-Graph x x
   refl-Reflexive-Graph = pr2 (pr2 G)
 ```
+
+## External links
+
+- [Reflexive graph](https://ncatlab.org/nlab/show/reflexive+graph) at nlab
+- [Graph](https://www.wikidata.org/wiki/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
diff --git a/src/graph-theory/regular-undirected-graphs.lagda.md b/src/graph-theory/regular-undirected-graphs.lagda.md
index 0d2f93eb6d..1ba8abaeae 100644
--- a/src/graph-theory/regular-undirected-graphs.lagda.md
+++ b/src/graph-theory/regular-undirected-graphs.lagda.md
@@ -19,8 +19,10 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-A regular undirected graph is a graph of which each vertex has the same number
-of incident edges
+A **regular undirected graph** is an
+[undirected graph](graph-theory.undirected-graphs.md) of which each vertex has
+the same number of
+[incident edges](graph-theory.neighbors-undirected-graphs.md).
 
 ## Definition
 
@@ -45,3 +47,11 @@ is-prop-is-regular-Undirected-Graph :
 is-prop-is-regular-Undirected-Graph X G =
   is-prop-type-Prop (is-regular-undirected-graph-Prop X G)
 ```
+
+## External links
+
+- [Regular graph](https://d3gt.com/unit.html?regular-graph) at D3 Graph Theory
+- [Regular graph](https://www.wikidata.org/wiki/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
diff --git a/src/graph-theory/simple-undirected-graphs.lagda.md b/src/graph-theory/simple-undirected-graphs.lagda.md
index 6b6dc1cb1d..8732d19fda 100644
--- a/src/graph-theory/simple-undirected-graphs.lagda.md
+++ b/src/graph-theory/simple-undirected-graphs.lagda.md
@@ -23,8 +23,10 @@ open import univalent-combinatorics.finite-types
 
 ## Idea
 
-An undirected graph is said to be simple if it only contains edges between
-distinct points, and there is at most one edge between any two vertices.
+An [undirected graph](graph-theory.undirected-graphs.md) is said to be
+**simple** if it only contains edges between
+[distinct points](foundation.pairs-of-distinct-elements.md), and there is at
+most one edge between any two vertices.
 
 ## Definition
 
@@ -62,3 +64,12 @@ Simple-Undirected-Graph l1 l2 =
         ( λ E →
           (x : V) → ¬ (type-Prop (E (pair (Fin-UU-Fin' 2) (λ y → x))))))
 ```
+
+## External links
+
+- [Graph](https://ncatlab.org/nlab/show/graph) at nlab
+- [Graph (discrete mathematics)](<https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)>)
+  at Wikipedia
+- [Simple graph](https://www.wikidata.org/wiki/Q15838309) on Wikidata
+- [Simple graph](https://mathworld.wolfram.com/SimpleGraph.html) at Wolfram
+  Mathworld
diff --git a/src/graph-theory/stereoisomerism-enriched-undirected-graphs.lagda.md b/src/graph-theory/stereoisomerism-enriched-undirected-graphs.lagda.md
index 629fcaf718..c14b20f5b7 100644
--- a/src/graph-theory/stereoisomerism-enriched-undirected-graphs.lagda.md
+++ b/src/graph-theory/stereoisomerism-enriched-undirected-graphs.lagda.md
@@ -20,12 +20,14 @@ open import graph-theory.equivalences-undirected-graphs
 
 ## Idea
 
-A stereoisomerism between two `(A,B)`-enriched undirected graphs is an
-equivalence between their underlying undirected graphs preserving the shape of
-the vertices. This concept is derived from the concept of stereoisomerism of
-chemical compounds.
+A **stereoisomerism** between two
+[`(A,B)`-enriched undirected graphs](graph-theory.enriched-undirected-graphs.md)
+is an [equivalence](graph-theory.equivalences-undirected-graphs.md) between
+their underlying [undirected graphs](graph-theory.undirected-graphs.md)
+preserving the shape of the vertices. This concept is derived from the concept
+of stereoisomerism of chemical compounds.
 
-Note: It could be that we only want the shapes to be merely preserved.
+**Note:** It could be that we only want the shapes to be merely preserved.
 
 ## Definition
 
@@ -50,3 +52,8 @@ module _
             ( undirected-graph-Enriched-Undirected-Graph A B H)
             ( e))))
 ```
+
+## External links
+
+- [Stereoisomerism](https://www.wikidata.org/wiki/Q47455153) on Wikidata
+- [Stereoisomerism](https://en.wikipedia.org/wiki/Stereoisomerism) at Wikipedia
diff --git a/src/graph-theory/totally-faithful-morphisms-undirected-graphs.lagda.md b/src/graph-theory/totally-faithful-morphisms-undirected-graphs.lagda.md
index 8ed518ea1f..4d140ac017 100644
--- a/src/graph-theory/totally-faithful-morphisms-undirected-graphs.lagda.md
+++ b/src/graph-theory/totally-faithful-morphisms-undirected-graphs.lagda.md
@@ -20,9 +20,10 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-A totally faithful morphism of undirected graphs is a morphism `f : G → H` of
-undirected graphs such that for edge `e` in `H` there is at most one edge in `G`
-that `f` maps to `e`.
+A **totally faithful morphism of undirected graphs** is a
+[morphism](graph-theory.morphisms-undirected-graphs.md) `f : G → H` of
+[undirected graphs](graph-theory.undirected-graphs.md) such that for edge `e` in
+`H` there is at most one edge in `G` that `f` maps to `e`.
 
 ## Definition
 
@@ -78,5 +79,11 @@ module _
 
 ## See also
 
-- Embeddings of undirected graphs
-- Faithful morphisms of undirected graphs
+- [Embeddings of undirected graphs](graph-theory.embeddings-undirected-graphs.md)
+- [Faithful morphisms of undirected graphs](graph-theory.faithful-morphisms-undirected-graphs.md)
+
+## External links
+
+- [Graph homomorphism](https://www.wikidata.org/wiki/Q3385162) on Wikidata
+- [Graph homomorphism](https://en.wikipedia.org/wiki/Graph_homomorphism) at
+  Wikipedia
diff --git a/src/graph-theory/trails-directed-graphs.lagda.md b/src/graph-theory/trails-directed-graphs.lagda.md
index 0c1bb636fd..2d3d950ac8 100644
--- a/src/graph-theory/trails-directed-graphs.lagda.md
+++ b/src/graph-theory/trails-directed-graphs.lagda.md
@@ -19,7 +19,9 @@ open import graph-theory.walks-directed-graphs
 
 ## Idea
 
-A trail in a directed graph is a walk that goes through each edge at most once.
+A **trail** in a [directed graph](graph-theory.directed-graphs.md) is a
+[walk](graph-theory.walks-directed-graphs.md) that goes through each edge at
+most once.
 
 ```agda
 module _
@@ -45,3 +47,10 @@ module _
     is-trail-walk-Directed-Graph (walk-trail-Directed-Graph t)
   is-trail-trail-Directed-Graph = pr2
 ```
+
+## External links
+
+- [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
+  Wikipedia
+- [Trail](https://www.wikidata.org/wiki/Q17455228) on Wikidata
+- [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 0b9ce40941..7b6e8eef9a 100644
--- a/src/graph-theory/trails-undirected-graphs.lagda.md
+++ b/src/graph-theory/trails-undirected-graphs.lagda.md
@@ -23,8 +23,9 @@ open import graph-theory.walks-undirected-graphs
 
 ## Idea
 
-A trail in an undirected graph is a walk that passes through each edge at most
-once
+A **trail** in an [undirected graph](graph-theory.undirected-graphs.md) is a
+[walk](graph-theory.walks-undirected-graphs.md) that passes through each edge at
+most once.
 
 ## Definition
 
@@ -158,12 +159,11 @@ module _
   second-segment-trail-Undirected-Graph t =
     second-segment-walk-Undirected-Graph G
       ( walk-trail-Undirected-Graph G t)
-{-
-  is-trail-first-walk-decomposition-trail-Undirected-Graph :
-    {y : vertex-Undirected-Graph G} (t : trail-Undirected-Graph G x y)
-    (v : vertex-on-walk-Undirected-Graph G (walk-trail-Undirected-Graph G t)) →
-    is-trail-walk-Undirected-Graph G
-      ( first-segment-trail-Undirected-Graph t v)
-  is-trail-first-walk-decomposition-trail-Undirected-Graph = {!!}
-  -}
 ```
+
+## External links
+
+- [Path (graph theory)](<https://en.wikipedia.org/wiki/Path_(graph_theory)>) at
+  Wikipedia
+- [Trail](https://www.wikidata.org/wiki/Q17455228) on Wikidata
+- [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 f015ee94f8..836f308b0f 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
@@ -24,3 +24,11 @@ open import univalent-combinatorics.standard-finite-types
 Undirected-Graph-Fin : UU (lsuc lzero)
 Undirected-Graph-Fin = Σ ℕ (λ V → unordered-pair (Fin V) → ℕ)
 ```
+
+## External links
+
+- [Graph](https://ncatlab.org/nlab/show/graph) at nlab
+- [Graph](https://www.wikidata.org/wiki/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
diff --git a/src/graph-theory/undirected-graphs.lagda.md b/src/graph-theory/undirected-graphs.lagda.md
index f7b5cbd8f5..0212e23e3d 100644
--- a/src/graph-theory/undirected-graphs.lagda.md
+++ b/src/graph-theory/undirected-graphs.lagda.md
@@ -21,8 +21,8 @@ open import graph-theory.directed-graphs
 
 ## Idea
 
-An undirected graph consists of a type `V` of vertices and a family `E` of types
-over the unordered pairs of `V`.
+An **undirected graph** consists of a type `V` of vertices and a family `E` of
+types over the [unordered pairs](foundation.unordered-pairs.md) of `V`.
 
 ## Definition
 
@@ -115,3 +115,11 @@ module _
   tr-edge-Undirected-Graph p q α =
     tr (edge-Undirected-Graph G) (eq-Eq-unordered-pair' p q α)
 ```
+
+## External links
+
+- [Graph](https://ncatlab.org/nlab/show/graph) at nlab
+- [Graph](https://www.wikidata.org/wiki/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
diff --git a/src/graph-theory/vertex-covers.lagda.md b/src/graph-theory/vertex-covers.lagda.md
index f8eddc1cec..f21d27a0c8 100644
--- a/src/graph-theory/vertex-covers.lagda.md
+++ b/src/graph-theory/vertex-covers.lagda.md
@@ -25,8 +25,8 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-A vertex cover on a undirect graph is a set of vertices that includes at least
-one extremity of each edge of the graph
+A **vertex cover** on a [undirect graph](graph-theory.undirected-graphs.md) is a
+set of vertices that includes at least one extremity of each edge of the graph.
 
 ## Definitions
 
@@ -42,3 +42,10 @@ vertex-cover G =
           ( Σ (vertex-Undirected-Graph G)
             ( λ x → is-in-unordered-pair p x × Id (c x) (inr star))))
 ```
+
+## External links
+
+- [Vertex cover](https://en.wikipedia.org/wiki/Vertex_cover) at Wikipedia
+- [Vertex cover](https://mathworld.wolfram.com/VertexCover.html) at Wolfram
+  Mathworld
+- [Vertex cover problem](https://www.wikidata.org/wiki/Q924362) on Wikidata
diff --git a/src/graph-theory/voltage-graphs.lagda.md b/src/graph-theory/voltage-graphs.lagda.md
index 279b1f5a89..bc99323d60 100644
--- a/src/graph-theory/voltage-graphs.lagda.md
+++ b/src/graph-theory/voltage-graphs.lagda.md
@@ -19,8 +19,9 @@ open import group-theory.groups
 
 ## Idea
 
-A voltage graph is a directed graph `G` equipped with a group `Π` (the voltage
-group) and a labelling of the edges of `G` by elements of `Π`.
+A **voltage graph** is a [directed graph](graph-theory.directed-graphs.md) `G`
+equipped with a [group](group-theory.groups.md) `Π`, which we call the **voltage
+group**, and a labelling of the edges of `G` by elements of `Π`.
 
 ## Definition
 
@@ -50,3 +51,7 @@ module _
     {x y : vertex-Voltage-Graph} → edge-Voltage-Graph x y → type-Group Π
   voltage-Voltage-Graph = pr2 G
 ```
+
+## External links
+
+- [Voltage graph](https://en.wikipedia.org/wiki/Voltage_graph) at Wikipedia
diff --git a/src/graph-theory/walks-directed-graphs.lagda.md b/src/graph-theory/walks-directed-graphs.lagda.md
index 2d67c73099..832a2352d8 100644
--- a/src/graph-theory/walks-directed-graphs.lagda.md
+++ b/src/graph-theory/walks-directed-graphs.lagda.md
@@ -36,10 +36,11 @@ open import graph-theory.morphisms-directed-graphs
 
 ## Idea
 
-A walk in a directed graph from a vertex `x` to a vertex `y` is a list of edges
-that connect `x` to `y`. Since every journey begins with a single step, we
-define the cons operation on walks in directed graphs with an edge from the
-source in the first argument, and a walk to the target in the second argument.
+A **walk** in a [directed graph](graph-theory.directed-graphs.md) from a vertex
+`x` to a vertex `y` is a [list](lists.lists.md) of edges that connect `x` to
+`y`. Since every journey begins with a single step, we define the `cons`
+operation on walks in directed graphs with an edge from the source in the first
+argument, and a walk to the target in the second argument.
 
 ## Definitions
 
@@ -779,3 +780,10 @@ module _
   walk-last-stage-walk-Directed-Graph e (cons-walk-Directed-Graph f w) =
     cons-walk-Directed-Graph e (walk-last-stage-walk-Directed-Graph f w)
 ```
+
+## External links
+
+- [Path](https://www.wikidata.org/wiki/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
diff --git a/src/graph-theory/walks-undirected-graphs.lagda.md b/src/graph-theory/walks-undirected-graphs.lagda.md
index 73fdd1a21c..d53552eb56 100644
--- a/src/graph-theory/walks-undirected-graphs.lagda.md
+++ b/src/graph-theory/walks-undirected-graphs.lagda.md
@@ -36,9 +36,10 @@ open import univalent-combinatorics.standard-finite-types
 
 ## Idea
 
-A walk in an undirected graph consists of a list of edges that connect the
-starting point with the end point. Walks may repeat edges and pass through the
-same vertex multiple times.
+A **walk** in an [undirected graph](graph-theory.undirected-graphs.md) consists
+of a [list](lists.lists.md) of edges that connect the starting point with the
+end point. Walks may repeat edges and pass through the same vertex multiple
+times.
 
 ## Definitions
 
@@ -512,3 +513,10 @@ module _
   eq-constant-walk-Undirected-Graph {y} =
     map-inv-is-equiv (is-equiv-constant-walk-eq-Undirected-Graph y)
 ```
+
+## External links
+
+- [Path](https://www.wikidata.org/wiki/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