chore: Concepts in graphs (#1646)

Author: fredrik-bakke

config/codespell-dictionary.txt

@@ -3,6 +3,7 @@ Kratowski->Kuratowski
 Kratowsky->Kuratowski
 Kuratowsky->Kuratowski
 Lavwere->Lawvere
+ahda->agda
 anamorhpism->anamorphism
 anamorhpisms->anamorphisms
 anamorhpsim->anamorphism

src/elementary-number-theory/bell-numbers.lagda.md

@@ -26,7 +26,7 @@ The {{#concept "Bell numbers" Agda=bell-number-ℕ WDID=Q816063 WD="Bell number"
 be defined recursively by $B_0 := 1$ and
 
 $$
-  B_{n+1} := \sum_{k=0}^{n} \binom{n}{k}B_k.
+  B_{n+1} := ∑_{k=0}^{n} \binom{n}{k}B_k.
 $$
 
 The Bell numbers are listed as sequence A000110 in the

src/elementary-number-theory/catalan-numbers.lagda.md

@@ -35,7 +35,7 @@ several combinatorics problems. The sequence starts
 
 The Catalan numbers may be defined by any of the formulas
 
-1. $C_{n + 1} = \sum_{k = 0}^n C_k C_{n-k}$, with $C_0 = 1$,
+1. $C_{n + 1} = ∑_{k = 0}^n C_k C_{n-k}$, with $C_0 = 1$,
 2. $C_n = {2n \choose n} - {2n \choose n + 1}$,
 3. $C_{n+1} = \frac{2(2n+1)}{n+2}C_n$, with $C_0 = 1$,
 4. $C_{n} = \frac{1}{n+1}{2n \choose n}$,
@@ -53,7 +53,7 @@ The Catalan numbers may be defined to be the sequence satisfying $C_0 = 1$ and
 the recurrence relation
 
 $$
-C_{n + 1} = \sum_{k = 0}^n C_k C_{n-k}.
+C_{n + 1} = ∑_{k = 0}^n C_k C_{n-k}.
 $$
 
 ```agda

src/graph-theory/circuits-undirected-graphs.lagda.md

@@ -21,7 +21,8 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-A {{#concept "circuit" Agda=circuit-Undirected-Graph WD="cycle" WDID=Q245595}}
+A
+{{#concept "circuit" Disambiguation="in an undirected graph" Agda=circuit-Undirected-Graph}}
 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)

src/graph-theory/connected-undirected-graphs.lagda.md

@@ -20,7 +20,8 @@ open import graph-theory.walks-undirected-graphs
 ## Idea
 
 An [undirected graph](graph-theory.undirected-graphs.md) is said to be
-**connected** if any point can be reached from any point by a
+{{#concept "connected" Disambiguation="undirected graph" WD="connected graph" WDID=Q230655 Agda=is-connected-Undirected-Graph}}
+if any point can be reached from any point by a
 [walk](graph-theory.walks-undirected-graphs.md).
 
 ## Definition

src/graph-theory/directed-graphs.lagda.md

@@ -18,25 +18,27 @@ open import foundation.universe-levels
 
 ## Idea
 
-A **directed graph** consists of a type of vertices equipped with a binary, type
-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.
+A
+{{#concept "directed graph" WD="directed graph" WDID=Q1137726 Agda=Directed-Graph}}
+consists of a type of vertices equipped with a binary, type 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](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
+[$Σ$-types](foundation.dependent-pair-types.md) preserve equivalences and a type
+family $A → U$ is equivalent to $∑_{(C : U)} C → A$ by
 [type duality](foundation.type-duality.md). Using these two observations we make
 the following calculation:
 
 $$
 \begin{equation}
 \begin{split}
-\sum_{(V\,:\,\mathcal{U})} (V \to V \to \mathcal{U}) & \simeq \sum_{(V\,:\,\mathcal{U})}
- (V \times V \to \mathcal{U}) \\
- &\simeq \sum_{(V,E\,:\,\mathcal{U})} (E \to (V \times V)) \\
-&\simeq  \sum_{(V,E\,:\,\mathcal{U})} ((E \to V) \times (E \to V))
+∑_{(V : 𝒰)} (V → V → 𝒰)
+  & ≃ ∑_{(V : 𝒰)} (V × V → 𝒰) \\
+  & ≃ ∑_{(V,E : 𝒰)} (E → (V × V)) \\
+  & ≃ ∑_{(V,E : 𝒰)} ((E → V) × (E → V))
 \end{split}
 \end{equation}
 $$

src/graph-theory/displayed-large-reflexive-graphs.lagda.md

@@ -18,7 +18,9 @@ open import graph-theory.reflexive-graphs
 
 ## Idea
 
-A {{#concept "displayed large reflexive graph"}} `H` a over a base
+A
+{{#concept "displayed large reflexive graph" Agda=Displayed-Large-Reflexive-Graph}}
+`H` a over a base
 [large reflexive graph](graph-theory.large-reflexive-graphs.md) `G` is the
 [structure](foundation.structure.md) of a dependent large reflexive graph over
 `G`. It consists of

src/graph-theory/edge-colored-undirected-graphs.lagda.md

@@ -20,9 +20,10 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-An **edge-colored undirected graph** is an
-[undirected graph](graph-theory.undirected-graphs.md) equipped with a family of
-maps `E p → X` from the edges at
+An
+{{#concept "edge-colored undirected graph" WD="edge-labeled graph" WDID=Q1541875 Agda=Edge-Colored-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 colors,
 such that the induced map `incident-Undirected-Graph G x → C` is
 [injective](foundation.injective-maps.md) for each vertex `x`.

src/graph-theory/embeddings-directed-graphs.lagda.md

@@ -20,11 +20,12 @@ open import graph-theory.morphisms-directed-graphs
 
 ## Idea
 
-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
+An
+{{#concept "embedding" Disambiguation="of directed graphs" Agda=is-emb-hom-Directed-Graph Agda=emb-Directed-Graph}}
+of [directed graphs](graph-theory.directed-graphs.md) is a
+[morphism](graph-theory.morphisms-directed-graphs.md) of directed graphs
+`f : G → H` 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

src/graph-theory/embeddings-undirected-graphs.lagda.md

@@ -20,11 +20,13 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-An **embedding of undirected graphs** is a
+An
+{{#concept "embedding" Disambiguation="of undirected graphs" Agda=is-emb-hom-Undirected-Graph Agda=emb-Undirected-Graph}}
+of [undirected graphs](graph-theory.undirected-graphs.md) 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
+undirected graphs 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 :