Adding external link sections

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,13 @@ is-acyclic-Undirected-Graph l G =
 ### Table of files related to cyclic types, groups, and rings
 
 {{#include tables/cyclic-types.md}}
+
+## External links
+
+- <a href="http://ul-fmf.github.io/MaGE/Q3115453" id="acyclic-undirected-graph">Acyclic
+  undirected graphs</a> at the Math Grand Exchange.
+- <a href="https://ncatlab.org/nlab/show/tree">Trees</a> at the nlab.
+- <a href="https://en.wikipedia.org/wiki/Tree_(graph_theory)#Forest">Forests</a>
+  at Wikipedia
+- <a href="https://mathworld.wolfram.com/AcyclicGraph.html">Acyclic graphs</a>
+  at Wolfram Mathworld.

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,12 @@ module _
       ( λ H →
         totally-faithful-hom-Undirected-Graph (undirected-graph-Polygon k H) G)
 ```
+
+## External links
+
+- <a href="http://ul-fmf.github.io/MaGE/Q245595" id="circuit-undirected-graph">Cycle</a>
+  at Math Grand Exchange
+- <a href="https://en.wikipedia.org/wiki/Cycle_(graph_theory)">Cycle (Graph
+  Theory)</a> at Wikipedia
+- <a href="https://mathworld.wolfram.com/GraphCycle.html">Graph Cycle</a> at
+  Wolfram Mathworld

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,12 @@ module _
   closed-walk-Undirected-Graph =
     Σ (Polygon k) (λ H → hom-Undirected-Graph (undirected-graph-Polygon k H) G)
 ```
+
+## External links
+
+- <a href="http://ul-fmf.github.io/MaGE/Q245595" id="closed-walk-undirected-graph">Cycle</a>
+  at Math Grand Exchange
+- <a href="https://en.wikipedia.org/wiki/Cycle_(graph_theory)">Cycle (Graph
+  Theory)</a> at Wikipedia
+- <a href="https://mathworld.wolfram.com/GraphCycle.html">Graph Cycle</a> at
+  Wolfram Mathworld

src/graph-theory/complete-bipartite-graphs.lagda.md

@@ -46,3 +46,16 @@ pr2 (complete-bipartite-Undirected-Graph-𝔽 X Y) p =
           ( element-unordered-pair p)
           ( inr y)))
 ```
+
+## External links
+
+- <a href="https://d3gt.com/unit.html?complete-bipartite">Complete bipartite
+  graphs</a> at D3 Graph Theory
+- <a href="http://ul-fmf.github.io/MaGE/Q913598" id="complete-bipartite-graph">Complete
+  bipartite graphs</a> at Math Grand Exchange
+- <a href="https://ncatlab.org/nlab/show/bipartite+graph">Bipartite graphs</a>
+  at nlab
+- <a href="https://en.wikipedia.org/wiki/Complete_bipartite_graph">Complete
+  bipartite graphs</a> at Wikipedia
+- <a href="https://mathworld.wolfram.com/CompleteBipartiteGraph.html">Complete
+  bipartite graphs</a> at Wolfram Mathworld