Adding more concept tags to graph theory (#953)

UniMath · Nov 28, 2023 · 81be903 · 81be903
1 parent 22b4bf4
commit 81be903
Show file tree

Hide file tree

Showing 4 changed files with 43 additions and 9 deletions.
diff --git a/src/graph-theory/closed-walks-undirected-graphs.lagda.md b/src/graph-theory/closed-walks-undirected-graphs.lagda.md
@@ -22,7 +22,7 @@ open import graph-theory.undirected-graphs
 ## Idea
 
 A
-{{#concept "closed walk" Agda=closed-walk-Undirected-Graph WDID=Q245595 WD="Cycle"}}
+{{#concept "closed walk" Agda=closed-walk-Undirected-Graph Disambiguation="undirected graph" WDID=Q245595 WD="Cycle"}}
 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`.

diff --git a/src/graph-theory/complete-undirected-graphs.lagda.md b/src/graph-theory/complete-undirected-graphs.lagda.md
@@ -19,9 +19,10 @@ open import univalent-combinatorics.finite-types
 
 ## Idea
 
-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
+A
+{{#concept "complete undirected graph" Agda=complete-Undirected-Graph-𝔽 WD="Complete graph" WDID=Q45715}}
+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.
 

diff --git 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](graph-theory.undirected-graphs.md) `G`
-consists of a [`k`-gon](graph-theory.polygons.md) `H` equipped with an
+A
+{{#concept "cycle" Agda=cycle-Undirected-Graph Disambiguation="undirected graph" WD="Cycle" WDID=Q245595}}
+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`.
 

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
@@ -17,11 +17,42 @@ open import univalent-combinatorics.standard-finite-types
 
 </details>
 
-## Definition
+## Idea
+
+A {{#concept "directed graph structure" WD="Directed graph" WDID=Q1137726}} on a
+[standard finite set](univalent-combinatorics.standard-finite-types.md) `Fin n`
+is a [binary type-valued relation](foundation.binary-relations.md)
+
+```text
+  Fin n → Fin n → 𝒰.
+```
+
+## Definitions
+
+### Directed graph structures on standard finite sets
+
+```agda
+structure-directed-graph-Fin : (l : Level) (n : ℕ) → UU (lsuc l)
+structure-directed-graph-Fin l n = Fin n → Fin n → UU l
+```
+
+### Directed graphs on standard finite sets
+
+```agda
+Directed-Graph-Fin : (l : Level) → UU (lsuc l)
+Directed-Graph-Fin l = Σ ℕ (structure-directed-graph-Fin l)
+```
+
+### Labeled finite directed graphs on standard finite sets
+
+A
+{{#concept "labeled finite directed graph" Agda=Labeled-Finite-Directed-Graph}}
+consists of a [natural number](elementary-number-theory.natural-numbers.md) `n`
+and a map `Fin n → Fin n → ℕ`.
 
 ```agda
-Directed-Graph-Fin : UU lzero
-Directed-Graph-Fin = Σ ℕ (λ V → Fin V → Fin V → ℕ)
+Labeled-Finite-Directed-Graph : UU lzero
+Labeled-Finite-Directed-Graph = Σ ℕ (λ n → Fin n → Fin n → ℕ)
 ```
 
 ## External links