Creating internal and external links in Graph Theory (#832)

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.

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

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

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

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

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

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

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

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

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

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

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

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