Adding concept tags to three files (#952)

Co-authored-by: Vojtěch Štěpančík <[email protected]>
UniMath · Nov 28, 2023 · 22b4bf4 · 22b4bf4
1 parent 2853b4e
commit 22b4bf4
Show file tree

Hide file tree

Showing 3 changed files with 133 additions and 40 deletions.
diff --git a/src/graph-theory/closed-walks-undirected-graphs.lagda.md b/src/graph-theory/closed-walks-undirected-graphs.lagda.md
@@ -21,10 +21,11 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-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`.
+A
+{{#concept "closed walk" Agda=closed-walk-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`.
 
 ## Definition
 

diff --git a/src/graph-theory/complete-bipartite-graphs.lagda.md b/src/graph-theory/complete-bipartite-graphs.lagda.md
@@ -23,28 +23,77 @@ open import univalent-combinatorics.finite-types
 
 </details>
 
+## Idea
+
+Consider two [finite sets](univalent-combinatorics.finite-types.md) `X` and `Y`.
+The
+{{#concept "complete bipartite graph" Agda=complete-bipartite-Undirected-Graph-𝔽 WDID=Q913598 WD="Complete bipartite graph"}}
+on `X` and `Y` is the [undirected finite graph](graph-theory.finite-graphs.md)
+consisting of:
+
+- The finite set of vertices is the
+  [coproduct type](univalent-combinatorics.coproduct-types.md) `X + Y`.
+- Given an [unordered pair](foundation.unordered-pairs.md) `f : I → X + Y` of
+  vertices, the finite type of edges on the unordered pair `(I , f)` is given by
+
+  ```text
+    (Σ (x : X), fiber f (inl x))  × (Σ (y : Y), fiber f (inr y)).
+  ```
+
+  In other words, an unordered pair of elements of the coproduct type `X + Y` is
+  an edge in the complete bipartite graph on `X` and `Y` precisely when one of
+  the elements of the unordered pair comes from `X` and the other comes from
+  `Y`.
+
 ## Definition
 
 ```agda
-complete-bipartite-Undirected-Graph-𝔽 :
-  {l1 l2 : Level} → 𝔽 l1 → 𝔽 l2 → Undirected-Graph-𝔽 (l1 ⊔ l2) (l1 ⊔ l2)
-pr1 (complete-bipartite-Undirected-Graph-𝔽 X Y) = coprod-𝔽 X Y
-pr2 (complete-bipartite-Undirected-Graph-𝔽 X Y) p =
-  prod-𝔽
-    ( Σ-𝔽 X
-      ( λ x →
-        fiber-𝔽
-          ( finite-type-2-Element-Type (pr1 p))
-          ( coprod-𝔽 X Y)
-          ( element-unordered-pair p)
-          ( inl x)))
-    ( Σ-𝔽 Y
-      ( λ y →
-        fiber-𝔽
-          ( finite-type-2-Element-Type (pr1 p))
-          ( coprod-𝔽 X Y)
-          ( element-unordered-pair p)
-          ( inr y)))
+module _
+  {l1 l2 : Level} (X : 𝔽 l1) (Y : 𝔽 l2)
+  where
+
+  vertex-finite-type-complete-bipartite-Undirected-Graph-𝔽 : 𝔽 (l1 ⊔ l2)
+  vertex-finite-type-complete-bipartite-Undirected-Graph-𝔽 = coprod-𝔽 X Y
+
+  vertex-complete-bipartite-Undirected-Graph-𝔽 : UU (l1 ⊔ l2)
+  vertex-complete-bipartite-Undirected-Graph-𝔽 =
+    type-𝔽 vertex-finite-type-complete-bipartite-Undirected-Graph-𝔽
+
+  unordered-pair-vertices-complete-bipartite-Undirected-Graph-𝔽 :
+    UU (lsuc lzero ⊔ l1 ⊔ l2)
+  unordered-pair-vertices-complete-bipartite-Undirected-Graph-𝔽 =
+    unordered-pair vertex-complete-bipartite-Undirected-Graph-𝔽
+
+  edge-finite-type-complete-bipartite-Undirected-Graph-𝔽 :
+    unordered-pair-vertices-complete-bipartite-Undirected-Graph-𝔽 → 𝔽 (l1 ⊔ l2)
+  edge-finite-type-complete-bipartite-Undirected-Graph-𝔽 p =
+    prod-𝔽
+      ( Σ-𝔽 X
+        ( λ x →
+          fiber-𝔽
+            ( finite-type-2-Element-Type (pr1 p))
+            ( coprod-𝔽 X Y)
+            ( element-unordered-pair p)
+            ( inl x)))
+      ( Σ-𝔽 Y
+        ( λ y →
+          fiber-𝔽
+            ( finite-type-2-Element-Type (pr1 p))
+            ( coprod-𝔽 X Y)
+            ( element-unordered-pair p)
+            ( inr y)))
+
+  edge-complete-bipartite-Undirected-Graph :
+    unordered-pair-vertices-complete-bipartite-Undirected-Graph-𝔽 → UU (l1 ⊔ l2)
+  edge-complete-bipartite-Undirected-Graph p =
+    type-𝔽 (edge-finite-type-complete-bipartite-Undirected-Graph-𝔽 p)
+
+  complete-bipartite-Undirected-Graph-𝔽 :
+    Undirected-Graph-𝔽 (l1 ⊔ l2) (l1 ⊔ l2)
+  pr1 complete-bipartite-Undirected-Graph-𝔽 =
+    vertex-finite-type-complete-bipartite-Undirected-Graph-𝔽
+  pr2 complete-bipartite-Undirected-Graph-𝔽 =
+    edge-finite-type-complete-bipartite-Undirected-Graph-𝔽
 ```
 
 ## External links

diff --git a/src/graph-theory/complete-multipartite-graphs.lagda.md b/src/graph-theory/complete-multipartite-graphs.lagda.md
@@ -24,25 +24,68 @@ open import univalent-combinatorics.function-types
 
 ## Idea
 
-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`.
+Consider a family of [finite types](univalent-combinatorics.finite-types.md) `Y`
+indexed by a finite type `X`. The
+{{#concept "complete multipartite graph" Agda=complete-multipartite-Undirected-Graph-𝔽 WD="Multipartite graph" WDID=Q1718082}}
+at `Y` is the [finite undirected graph](graph-theory.finite-graphs.md)
+consisting of:
+
+- The finite type of vertices is the
+  [dependent pair type](univalent-combinatorics.dependent-pair-types.md)
+  `Σ (x : X), Y x`.
+- An [unordered pair](foundation.unordered-pairs.md) `f : I → Σ (x : X), Y x` is
+  an edge if the induced unordered pair `pr1 ∘ f : I → X` is an
+  [embedding](foundation-core.embeddings.md).
+
+**Note:** The formalization of the finite type of edges below is different from
+the above description, and needs to be changed.
+
+## Definitions
+
+### Complete multipartite graphs
 
 ```agda
-complete-multipartite-Undirected-Graph-𝔽 :
-  {l1 l2 : Level} (X : 𝔽 l1) (Y : type-𝔽 X → 𝔽 l2) →
-  Undirected-Graph-𝔽 (l1 ⊔ l2) l1
-pr1 (complete-multipartite-Undirected-Graph-𝔽 X Y) = Σ-𝔽 X Y
-pr2 (complete-multipartite-Undirected-Graph-𝔽 X Y) p =
-  ( Π-𝔽 ( finite-type-2-Element-Type (pr1 p))
-        ( λ x →
-          Π-𝔽 ( finite-type-2-Element-Type (pr1 p))
-              ( λ y →
-                Id-𝔽 X
-                  ( pr1 (element-unordered-pair p x))
-                  ( pr1 (element-unordered-pair p y))))) →-𝔽
-  empty-𝔽
+module _
+  {l1 l2 : Level} (X : 𝔽 l1) (Y : type-𝔽 X → 𝔽 l2)
+  where
+
+  vertex-finite-type-complete-multipartite-Undirected-Graph-𝔽 : 𝔽 (l1 ⊔ l2)
+  vertex-finite-type-complete-multipartite-Undirected-Graph-𝔽 =
+    Σ-𝔽 X Y
+
+  vertex-complete-multipartite-Undirected-Graph-𝔽 : UU (l1 ⊔ l2)
+  vertex-complete-multipartite-Undirected-Graph-𝔽 =
+    type-𝔽 vertex-finite-type-complete-multipartite-Undirected-Graph-𝔽
+
+  unordered-pair-vertices-complete-multipartite-Undirected-Graph-𝔽 :
+    UU (lsuc lzero ⊔ l1 ⊔ l2)
+  unordered-pair-vertices-complete-multipartite-Undirected-Graph-𝔽 =
+    unordered-pair vertex-complete-multipartite-Undirected-Graph-𝔽
+
+  edge-finite-type-complete-multipartite-Undirected-Graph-𝔽 :
+    unordered-pair-vertices-complete-multipartite-Undirected-Graph-𝔽 → 𝔽 l1
+  edge-finite-type-complete-multipartite-Undirected-Graph-𝔽 p =
+    ( Π-𝔽
+      ( finite-type-2-Element-Type (pr1 p))
+      ( λ x →
+        Π-𝔽
+          ( finite-type-2-Element-Type (pr1 p))
+          ( λ y →
+            Id-𝔽 X
+              ( pr1 (element-unordered-pair p x))
+              ( pr1 (element-unordered-pair p y))))) →-𝔽
+    ( empty-𝔽)
+
+  edge-complete-multipartite-Undirected-Graph-𝔽 :
+    unordered-pair-vertices-complete-multipartite-Undirected-Graph-𝔽 → UU l1
+  edge-complete-multipartite-Undirected-Graph-𝔽 p =
+    type-𝔽 (edge-finite-type-complete-multipartite-Undirected-Graph-𝔽 p)
+
+  complete-multipartite-Undirected-Graph-𝔽 : Undirected-Graph-𝔽 (l1 ⊔ l2) l1
+  pr1 complete-multipartite-Undirected-Graph-𝔽 =
+    vertex-finite-type-complete-multipartite-Undirected-Graph-𝔽
+  pr2 complete-multipartite-Undirected-Graph-𝔽 =
+    edge-finite-type-complete-multipartite-Undirected-Graph-𝔽
 ```
 
 ## External links