diff --git a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
index 5dc0be6bfb..20b148c940 100644
--- a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
+++ b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
@@ -123,7 +123,8 @@ module _
     D ( n +ℕ 2)
       ( raise-Fin l1 (n +ℕ 2) ,
         unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))
-  ( not-R-transposition-fin-succ-succ : (n : ℕ) →
+  ( not-R-transposition-fin-succ-succ :
+    (n : ℕ) →
     ( Y : 2-Element-Decidable-Subtype l1 (raise-Fin l1 (n +ℕ 2))) →
     ¬ ( sim-Equivalence-Relation
       ( R
diff --git a/src/foundation/decidable-equality.lagda.md b/src/foundation/decidable-equality.lagda.md
index aba53c004a..54fe5f5219 100644
--- a/src/foundation/decidable-equality.lagda.md
+++ b/src/foundation/decidable-equality.lagda.md
@@ -33,11 +33,15 @@ open import foundation-core.transport-along-identifications
 
 </details>
 
-## Definition
+## Idea
 
 A type `A` is said to have **decidable equality** if `x ＝ y` is a
 [decidable type](foundation.decidable-types.md) for every `x y : A`.
 
+## Definitions
+
+### The predicate of having decidable equality
+
 ```agda
 has-decidable-equality : {l : Level} (A : UU l) → UU l
 has-decidable-equality A = (x y : A) → is-decidable (x ＝ y)
diff --git a/src/foundation/symmetric-cores-binary-relations.lagda.md b/src/foundation/symmetric-cores-binary-relations.lagda.md
index e1c5e5fa32..e42c4546bd 100644
--- a/src/foundation/symmetric-cores-binary-relations.lagda.md
+++ b/src/foundation/symmetric-cores-binary-relations.lagda.md
@@ -10,7 +10,6 @@ module foundation.symmetric-cores-binary-relations where
 
 ```agda
 open import foundation.binary-relations
-open import foundation.equivalences
 open import foundation.functoriality-dependent-function-types
 open import foundation.functoriality-function-types
 open import foundation.morphisms-binary-relations
@@ -20,6 +19,8 @@ open import foundation.type-arithmetic-dependent-function-types
 open import foundation.universe-levels
 open import foundation.unordered-pairs
 
+open import foundation-core.equivalences
+
 open import univalent-combinatorics.standard-finite-types
 ```
 
diff --git a/src/graph-theory.lagda.md b/src/graph-theory.lagda.md
index 2c52f7b232..24b9804638 100644
--- a/src/graph-theory.lagda.md
+++ b/src/graph-theory.lagda.md
@@ -25,7 +25,9 @@ open import graph-theory.equivalences-undirected-graphs public
 open import graph-theory.eulerian-circuits-undirected-graphs public
 open import graph-theory.faithful-morphisms-undirected-graphs public
 open import graph-theory.fibers-directed-graphs public
-open import graph-theory.finite-graphs public
+open import graph-theory.finite-undirected-graphs public
+open import graph-theory.forgetful-functor-from-directed-graphs-to-undirected-graphs public
+open import graph-theory.forgetful-functor-from-undirected-graphs-to-directed-graphs public
 open import graph-theory.geometric-realizations-undirected-graphs public
 open import graph-theory.hypergraphs public
 open import graph-theory.matchings public
@@ -45,10 +47,12 @@ open import graph-theory.stereoisomerism-enriched-undirected-graphs public
 open import graph-theory.totally-faithful-morphisms-undirected-graphs public
 open import graph-theory.trails-directed-graphs public
 open import graph-theory.trails-undirected-graphs public
+open import graph-theory.undirected-core-directed-graphs public
 open import graph-theory.undirected-graph-structures-on-standard-finite-sets public
 open import graph-theory.undirected-graphs public
 open import graph-theory.vertex-covers public
 open import graph-theory.voltage-graphs public
 open import graph-theory.walks-directed-graphs public
+open import graph-theory.walks-finite-undirected-graphs public
 open import graph-theory.walks-undirected-graphs public
 ```
diff --git a/src/graph-theory/complete-bipartite-graphs.lagda.md b/src/graph-theory/complete-bipartite-graphs.lagda.md
index aaa1bba60e..40cb9f4c79 100644
--- a/src/graph-theory/complete-bipartite-graphs.lagda.md
+++ b/src/graph-theory/complete-bipartite-graphs.lagda.md
@@ -11,7 +11,7 @@ open import foundation.coproduct-types
 open import foundation.universe-levels
 open import foundation.unordered-pairs
 
-open import graph-theory.finite-graphs
+open import graph-theory.finite-undirected-graphs
 
 open import univalent-combinatorics.2-element-types
 open import univalent-combinatorics.cartesian-product-types
diff --git a/src/graph-theory/complete-multipartite-graphs.lagda.md b/src/graph-theory/complete-multipartite-graphs.lagda.md
index ec08c569d1..fae66c6658 100644
--- a/src/graph-theory/complete-multipartite-graphs.lagda.md
+++ b/src/graph-theory/complete-multipartite-graphs.lagda.md
@@ -10,7 +10,7 @@ module graph-theory.complete-multipartite-graphs where
 open import foundation.universe-levels
 open import foundation.unordered-pairs
 
-open import graph-theory.finite-graphs
+open import graph-theory.finite-undirected-graphs
 
 open import univalent-combinatorics.2-element-types
 open import univalent-combinatorics.dependent-function-types
diff --git a/src/graph-theory/complete-undirected-graphs.lagda.md b/src/graph-theory/complete-undirected-graphs.lagda.md
index 69dddf5784..c13e35221c 100644
--- a/src/graph-theory/complete-undirected-graphs.lagda.md
+++ b/src/graph-theory/complete-undirected-graphs.lagda.md
@@ -10,7 +10,7 @@ module graph-theory.complete-undirected-graphs where
 open import foundation.universe-levels
 
 open import graph-theory.complete-multipartite-graphs
-open import graph-theory.finite-graphs
+open import graph-theory.finite-undirected-graphs
 
 open import univalent-combinatorics.finite-types
 ```
diff --git a/src/graph-theory/embeddings-directed-graphs.lagda.md b/src/graph-theory/embeddings-directed-graphs.lagda.md
index 16d08fb0bf..851426f6a2 100644
--- a/src/graph-theory/embeddings-directed-graphs.lagda.md
+++ b/src/graph-theory/embeddings-directed-graphs.lagda.md
@@ -44,9 +44,9 @@ module _
   {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
   where
 
-  is-emb-hom-Directed-Graph-Prop :
+  is-emb-prop-hom-Directed-Graph :
     hom-Directed-Graph G H → Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  is-emb-hom-Directed-Graph-Prop f =
+  is-emb-prop-hom-Directed-Graph f =
     prod-Prop
       ( is-emb-Prop (vertex-hom-Directed-Graph G H f))
       ( Π-Prop
@@ -57,7 +57,7 @@ module _
             ( λ y → is-emb-Prop (edge-hom-Directed-Graph G H f {x} {y}))))
 
   is-emb-hom-Directed-Graph : hom-Directed-Graph G H → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  is-emb-hom-Directed-Graph f = type-Prop (is-emb-hom-Directed-Graph-Prop f)
+  is-emb-hom-Directed-Graph f = type-Prop (is-emb-prop-hom-Directed-Graph f)
 
   emb-Directed-Graph : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
   emb-Directed-Graph = Σ (hom-Directed-Graph G H) is-emb-hom-Directed-Graph
diff --git a/src/graph-theory/embeddings-undirected-graphs.lagda.md b/src/graph-theory/embeddings-undirected-graphs.lagda.md
index 809f8e1a3c..6e2a92d738 100644
--- a/src/graph-theory/embeddings-undirected-graphs.lagda.md
+++ b/src/graph-theory/embeddings-undirected-graphs.lagda.md
@@ -47,9 +47,9 @@ module _
   (G : Undirected-Graph l1 l2) (H : Undirected-Graph l3 l4)
   where
 
-  is-emb-hom-undirected-graph-Prop :
+  is-emb-prop-hom-Undirected-Graph :
     hom-Undirected-Graph G H → Prop (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  is-emb-hom-undirected-graph-Prop f =
+  is-emb-prop-hom-Undirected-Graph f =
     prod-Prop
       ( is-emb-Prop (vertex-hom-Undirected-Graph G H f))
       ( Π-Prop
@@ -59,12 +59,12 @@ module _
 
   is-emb-hom-Undirected-Graph :
     hom-Undirected-Graph G H → UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  is-emb-hom-Undirected-Graph f = type-Prop (is-emb-hom-undirected-graph-Prop f)
+  is-emb-hom-Undirected-Graph f = type-Prop (is-emb-prop-hom-Undirected-Graph f)
 
   is-prop-is-emb-hom-Undirected-Graph :
     (f : hom-Undirected-Graph G H) → is-prop (is-emb-hom-Undirected-Graph f)
   is-prop-is-emb-hom-Undirected-Graph f =
-    is-prop-type-Prop (is-emb-hom-undirected-graph-Prop f)
+    is-prop-type-Prop (is-emb-prop-hom-Undirected-Graph f)
 
   emb-Undirected-Graph : UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
   emb-Undirected-Graph =
diff --git a/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md b/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md
index 685ec29151..5105450834 100644
--- a/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md
+++ b/src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md
@@ -42,9 +42,9 @@ module _
   (G : Undirected-Graph l1 l2) (H : Undirected-Graph l3 l4)
   where
 
-  is-faithful-hom-undirected-graph-Prop :
+  is-faithful-prop-hom-Undirected-Graph :
     hom-Undirected-Graph G H → Prop (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l4)
-  is-faithful-hom-undirected-graph-Prop f =
+  is-faithful-prop-hom-Undirected-Graph f =
     Π-Prop
       ( unordered-pair-vertices-Undirected-Graph G)
       ( λ p → is-emb-Prop (edge-hom-Undirected-Graph G H f p))
@@ -52,13 +52,13 @@ module _
   is-faithful-hom-Undirected-Graph :
     hom-Undirected-Graph G H → UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l4)
   is-faithful-hom-Undirected-Graph f =
-    type-Prop (is-faithful-hom-undirected-graph-Prop f)
+    type-Prop (is-faithful-prop-hom-Undirected-Graph f)
 
   is-prop-is-faithful-hom-Undirected-Graph :
     (f : hom-Undirected-Graph G H) →
     is-prop (is-faithful-hom-Undirected-Graph f)
   is-prop-is-faithful-hom-Undirected-Graph f =
-    is-prop-type-Prop (is-faithful-hom-undirected-graph-Prop f)
+    is-prop-type-Prop (is-faithful-prop-hom-Undirected-Graph f)
 
   faithful-hom-Undirected-Graph : UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
   faithful-hom-Undirected-Graph =
diff --git a/src/graph-theory/finite-graphs.lagda.md b/src/graph-theory/finite-undirected-graphs.lagda.md
similarity index 56%
rename from src/graph-theory/finite-graphs.lagda.md
rename to src/graph-theory/finite-undirected-graphs.lagda.md
index 6ffc64905b..9dedac0ab3 100644
--- a/src/graph-theory/finite-graphs.lagda.md
+++ b/src/graph-theory/finite-undirected-graphs.lagda.md
@@ -1,22 +1,29 @@
-# Finite graphs
+# Finite undirected graphs
 
 ```agda
-module graph-theory.finite-graphs where
+module graph-theory.finite-undirected-graphs where
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.decidable-equality
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.fibers-of-maps
 open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
+open import foundation.propositions
+open import foundation.sets
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.type-theoretic-principle-of-choice
 open import foundation.universe-levels
 open import foundation.unordered-pairs
 
 open import graph-theory.undirected-graphs
 
+open import univalent-combinatorics.equality-finite-types
 open import univalent-combinatorics.finite-types
 ```
 
@@ -25,7 +32,7 @@ open import univalent-combinatorics.finite-types
 ## Idea
 
 A **finite undirected graph** consists of a
-[finite set](univalent-combinatorics.finite-types.md) of vertices and a family
+[finite type](univalent-combinatorics.finite-types.md) of vertices and a family
 of finite types of edges indexed by
 [unordered pairs](foundation.unordered-pairs.md) of vertices.
 
@@ -35,6 +42,31 @@ is also common to call such graphs _multigraphs_.
 
 ## Definitions
 
+### The predicate of being a finite undirected graph
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph l1 l2)
+  where
+
+  is-finite-prop-Undirected-Graph : Prop (lsuc lzero ⊔ l1 ⊔ l2)
+  is-finite-prop-Undirected-Graph =
+    prod-Prop
+      ( is-finite-Prop (vertex-Undirected-Graph G))
+      ( Π-Prop
+        ( unordered-pair-vertices-Undirected-Graph G)
+        ( λ p → is-finite-Prop (edge-Undirected-Graph G p)))
+
+  is-finite-Undirected-Graph : UU (lsuc lzero ⊔ l1 ⊔ l2)
+  is-finite-Undirected-Graph =
+    type-Prop is-finite-prop-Undirected-Graph
+
+  is-prop-is-finite-Undirected-Graph :
+    is-prop is-finite-Undirected-Graph
+  is-prop-is-finite-Undirected-Graph =
+    is-prop-type-Prop is-finite-prop-Undirected-Graph
+```
+
 ### Finite undirected graphs
 
 ```agda
@@ -55,6 +87,15 @@ module _
   is-finite-vertex-Undirected-Graph-𝔽 : is-finite vertex-Undirected-Graph-𝔽
   is-finite-vertex-Undirected-Graph-𝔽 = is-finite-type-𝔽 (pr1 G)
 
+  is-set-vertex-Undirected-Graph-𝔽 : is-set vertex-Undirected-Graph-𝔽
+  is-set-vertex-Undirected-Graph-𝔽 =
+    is-set-is-finite is-finite-vertex-Undirected-Graph-𝔽
+
+  has-decidable-equality-vertex-Undirected-Graph-𝔽 :
+    has-decidable-equality vertex-Undirected-Graph-𝔽
+  has-decidable-equality-vertex-Undirected-Graph-𝔽 =
+    has-decidable-equality-is-finite is-finite-vertex-Undirected-Graph-𝔽
+
   edge-Undirected-Graph-𝔽 :
     (p : unordered-pair-vertices-Undirected-Graph-𝔽) → UU l2
   edge-Undirected-Graph-𝔽 p = type-𝔽 (pr2 G p)
@@ -64,6 +105,18 @@ module _
     is-finite (edge-Undirected-Graph-𝔽 p)
   is-finite-edge-Undirected-Graph-𝔽 p = is-finite-type-𝔽 (pr2 G p)
 
+  is-set-edge-Undirected-Graph-𝔽 :
+    (p : unordered-pair-vertices-Undirected-Graph-𝔽) →
+    is-set (edge-Undirected-Graph-𝔽 p)
+  is-set-edge-Undirected-Graph-𝔽 p =
+    is-set-is-finite (is-finite-edge-Undirected-Graph-𝔽 p)
+
+  has-decidable-equality-edge-Undirected-Graph-𝔽 :
+    (p : unordered-pair-vertices-Undirected-Graph-𝔽) →
+    has-decidable-equality (edge-Undirected-Graph-𝔽 p)
+  has-decidable-equality-edge-Undirected-Graph-𝔽 p =
+    has-decidable-equality-is-finite (is-finite-edge-Undirected-Graph-𝔽 p)
+
   total-edge-Undirected-Graph-𝔽 : UU (lsuc lzero ⊔ l1 ⊔ l2)
   total-edge-Undirected-Graph-𝔽 =
     Σ unordered-pair-vertices-Undirected-Graph-𝔽 edge-Undirected-Graph-𝔽
@@ -71,6 +124,19 @@ module _
   undirected-graph-Undirected-Graph-𝔽 : Undirected-Graph l1 l2
   pr1 undirected-graph-Undirected-Graph-𝔽 = vertex-Undirected-Graph-𝔽
   pr2 undirected-graph-Undirected-Graph-𝔽 = edge-Undirected-Graph-𝔽
+
+  is-finite-Undirected-Graph-𝔽 :
+    is-finite-Undirected-Graph undirected-graph-Undirected-Graph-𝔽
+  pr1 is-finite-Undirected-Graph-𝔽 = is-finite-vertex-Undirected-Graph-𝔽
+  pr2 is-finite-Undirected-Graph-𝔽 = is-finite-edge-Undirected-Graph-𝔽
+
+compute-Undirected-Graph-𝔽 :
+  {l1 l2 : Level} →
+  Σ (Undirected-Graph l1 l2) is-finite-Undirected-Graph ≃
+  Undirected-Graph-𝔽 l1 l2
+compute-Undirected-Graph-𝔽 =
+  ( equiv-tot (λ V → inv-distributive-Π-Σ)) ∘e
+  ( interchange-Σ-Σ _)
 ```
 
 ### The following type is expected to be equivalent to Undirected-Graph-𝔽
diff --git a/src/graph-theory/forgetful-functor-from-directed-graphs-to-undirected-graphs.lagda.md b/src/graph-theory/forgetful-functor-from-directed-graphs-to-undirected-graphs.lagda.md
new file mode 100644
index 0000000000..f348816c31
--- /dev/null
+++ b/src/graph-theory/forgetful-functor-from-directed-graphs-to-undirected-graphs.lagda.md
@@ -0,0 +1,49 @@
+# The forgetful functor from directed graphs to undirected graphs
+
+```agda
+module
+  graph-theory.forgetful-functor-from-directed-graphs-to-undirected-graphs
+  where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.symmetric-binary-relations
+open import foundation.universe-levels
+
+open import graph-theory.directed-graphs
+open import graph-theory.undirected-graphs
+```
+
+</details>
+
+## Idea
+
+The **forgetful functor** from
+[directed graphs](graph-theory.directed-graphs.md) to
+[undirected graphs](graph-theory.undirected-graphs.md) forgets the direction of
+directed edges.
+
+## Definitions
+
+### The operation on directed graphs that forgets the directions of the edges
+
+```agda
+module _
+  {l1 l2 : Level} (G : Directed-Graph l1 l2)
+  where
+
+  vertex-undirected-graph-Directed-Graph : UU l1
+  vertex-undirected-graph-Directed-Graph = vertex-Directed-Graph G
+
+  edge-undirected-graph-Directed-Graph :
+    Symmetric-Relation l2 vertex-undirected-graph-Directed-Graph
+  edge-undirected-graph-Directed-Graph =
+    symmetric-relation-Relation (edge-Directed-Graph G)
+
+  undirected-graph-Graph : Undirected-Graph l1 l2
+  pr1 undirected-graph-Graph = vertex-undirected-graph-Directed-Graph
+  pr2 undirected-graph-Graph = edge-undirected-graph-Directed-Graph
+```
diff --git a/src/graph-theory/forgetful-functor-from-undirected-graphs-to-directed-graphs.lagda.md b/src/graph-theory/forgetful-functor-from-undirected-graphs-to-directed-graphs.lagda.md
new file mode 100644
index 0000000000..7ccfd503fe
--- /dev/null
+++ b/src/graph-theory/forgetful-functor-from-undirected-graphs-to-directed-graphs.lagda.md
@@ -0,0 +1,73 @@
+# The forgetful functor from undirected graphs to directed graphs
+
+```agda
+module
+  graph-theory.forgetful-functor-from-undirected-graphs-to-directed-graphs
+  where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+open import foundation.unordered-pairs
+
+open import graph-theory.directed-graphs
+open import graph-theory.undirected-graphs
+```
+
+</details>
+
+## Idea
+
+The **forgetful functor** from
+[undirected graphs](graph-theory.undirected-graphs.md) to
+[directed graphs](graph-theory.directed-graphs.md) takes an undirected graph `G`
+and returns the directed graphs in which we have an edge from both `x` to `y`
+and from `y` to `x` for every undirected edge on the
+[standard unordered pair](foundation.unordered-pairs.md) `{x,y}`.
+
+## Definitions
+
+### The forgetful functor from undirected graphs to directed graphs
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph l1 l2)
+  where
+
+  vertex-graph-Undirected-Graph : UU l1
+  vertex-graph-Undirected-Graph = vertex-Undirected-Graph G
+
+  edge-graph-Undirected-Graph :
+    (x y : vertex-graph-Undirected-Graph) → UU l2
+  edge-graph-Undirected-Graph x y =
+    edge-Undirected-Graph G (standard-unordered-pair x y)
+
+  graph-Undirected-Graph : Directed-Graph l1 l2
+  pr1 graph-Undirected-Graph = vertex-graph-Undirected-Graph
+  pr2 graph-Undirected-Graph = edge-graph-Undirected-Graph
+
+  directed-edge-edge-Undirected-Graph :
+    (p : unordered-pair-vertices-Undirected-Graph G)
+    (e : edge-Undirected-Graph G p)
+    (i : type-unordered-pair p) →
+    edge-graph-Undirected-Graph
+      ( element-unordered-pair p i)
+      ( other-element-unordered-pair p i)
+  directed-edge-edge-Undirected-Graph p e i =
+    tr-edge-Undirected-Graph G
+      ( p)
+      ( standard-unordered-pair
+        ( element-unordered-pair p i)
+        ( other-element-unordered-pair p i))
+      ( inv-Eq-unordered-pair
+        ( standard-unordered-pair
+          ( element-unordered-pair p i)
+          ( other-element-unordered-pair p i))
+        ( p)
+        ( compute-standard-unordered-pair-element-unordered-pair p i))
+      ( e)
+```
diff --git a/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md b/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md
index d4fca9ade5..43d80d7aae 100644
--- a/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md
+++ b/src/graph-theory/mere-equivalences-undirected-graphs.lagda.md
@@ -33,15 +33,15 @@ module _
   (G : Undirected-Graph l1 l2) (H : Undirected-Graph l3 l4)
   where
 
-  mere-equiv-Undirected-Graph-Prop : Prop (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  mere-equiv-Undirected-Graph-Prop = trunc-Prop (equiv-Undirected-Graph G H)
+  mere-equiv-prop-Undirected-Graph : Prop (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  mere-equiv-prop-Undirected-Graph = trunc-Prop (equiv-Undirected-Graph G H)
 
   mere-equiv-Undirected-Graph : UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  mere-equiv-Undirected-Graph = type-Prop mere-equiv-Undirected-Graph-Prop
+  mere-equiv-Undirected-Graph = type-Prop mere-equiv-prop-Undirected-Graph
 
   is-prop-mere-equiv-Undirected-Graph : is-prop mere-equiv-Undirected-Graph
   is-prop-mere-equiv-Undirected-Graph =
-    is-prop-type-Prop mere-equiv-Undirected-Graph-Prop
+    is-prop-type-Prop mere-equiv-prop-Undirected-Graph
 ```
 
 ## Properties
diff --git a/src/graph-theory/neighbors-undirected-graphs.lagda.md b/src/graph-theory/neighbors-undirected-graphs.lagda.md
index cfad0b538c..a867895e80 100644
--- a/src/graph-theory/neighbors-undirected-graphs.lagda.md
+++ b/src/graph-theory/neighbors-undirected-graphs.lagda.md
@@ -25,10 +25,13 @@ open import graph-theory.undirected-graphs
 
 ## Idea
 
-The type of neighbors a vertex `x` of an undirected graph `G` is the type of all
+The type of **neighbors** of a vertex `x` of an
+[undirected graph](graph-theory.undirected-graphs.md) `G` is the type of all
 vertices `y` in `G` equipped with an edge from `x` to `y`.
 
-## Definition
+## Definitions
+
+### The type of neighbors of an element in an undirected graph
 
 ```agda
 module _
diff --git a/src/graph-theory/regular-undirected-graphs.lagda.md b/src/graph-theory/regular-undirected-graphs.lagda.md
index 8b64834fa1..d8071e111b 100644
--- a/src/graph-theory/regular-undirected-graphs.lagda.md
+++ b/src/graph-theory/regular-undirected-graphs.lagda.md
@@ -27,10 +27,10 @@ the same number of
 ## Definition
 
 ```agda
-is-regular-undirected-graph-Prop :
+is-regular-prop-Undirected-Graph :
   {l1 l2 l3 : Level} (X : UU l1)
   (G : Undirected-Graph l2 l3) → Prop (l1 ⊔ l2 ⊔ l3)
-is-regular-undirected-graph-Prop X G =
+is-regular-prop-Undirected-Graph X G =
   Π-Prop
     ( vertex-Undirected-Graph G)
     ( λ x → mere-equiv-Prop X (neighbor-Undirected-Graph G x))
@@ -39,13 +39,13 @@ is-regular-Undirected-Graph :
   {l1 l2 l3 : Level} (X : UU l1) (G : Undirected-Graph l2 l3) →
   UU (l1 ⊔ l2 ⊔ l3)
 is-regular-Undirected-Graph X G =
-  type-Prop (is-regular-undirected-graph-Prop X G)
+  type-Prop (is-regular-prop-Undirected-Graph X G)
 
 is-prop-is-regular-Undirected-Graph :
   {l1 l2 l3 : Level} (X : UU l1) (G : Undirected-Graph l2 l3) →
   is-prop (is-regular-Undirected-Graph X G)
 is-prop-is-regular-Undirected-Graph X G =
-  is-prop-type-Prop (is-regular-undirected-graph-Prop X G)
+  is-prop-type-Prop (is-regular-prop-Undirected-Graph X G)
 ```
 
 ## External links
diff --git a/src/graph-theory/simple-undirected-graphs.lagda.md b/src/graph-theory/simple-undirected-graphs.lagda.md
index 4d133c9dc9..60733aff3f 100644
--- a/src/graph-theory/simple-undirected-graphs.lagda.md
+++ b/src/graph-theory/simple-undirected-graphs.lagda.md
@@ -35,8 +35,8 @@ module _
   {l1 l2 : Level} (G : Undirected-Graph l1 l2)
   where
 
-  is-simple-Undirected-Graph-Prop : Prop (lsuc lzero ⊔ l1 ⊔ l2)
-  is-simple-Undirected-Graph-Prop =
+  is-simple-prop-Undirected-Graph : Prop (lsuc lzero ⊔ l1 ⊔ l2)
+  is-simple-prop-Undirected-Graph =
     prod-Prop
       ( Π-Prop
         ( unordered-pair-vertices-Undirected-Graph G)
@@ -50,11 +50,11 @@ module _
         ( λ p → is-prop-Prop (edge-Undirected-Graph G p)))
 
   is-simple-Undirected-Graph : UU (lsuc lzero ⊔ l1 ⊔ l2)
-  is-simple-Undirected-Graph = type-Prop is-simple-Undirected-Graph-Prop
+  is-simple-Undirected-Graph = type-Prop is-simple-prop-Undirected-Graph
 
   is-prop-is-simple-Undirected-Graph : is-prop is-simple-Undirected-Graph
   is-prop-is-simple-Undirected-Graph =
-    is-prop-type-Prop is-simple-Undirected-Graph-Prop
+    is-prop-type-Prop is-simple-prop-Undirected-Graph
 
 Simple-Undirected-Graph : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
 Simple-Undirected-Graph l1 l2 =
diff --git a/src/graph-theory/trails-undirected-graphs.lagda.md b/src/graph-theory/trails-undirected-graphs.lagda.md
index b26efaa0cb..1f83bcab54 100644
--- a/src/graph-theory/trails-undirected-graphs.lagda.md
+++ b/src/graph-theory/trails-undirected-graphs.lagda.md
@@ -98,11 +98,11 @@ module _
   length-trail-Undirected-Graph t =
     length-walk-Undirected-Graph G (walk-trail-Undirected-Graph t)
 
-  is-constant-trail-Undirected-Graph-Prop :
+  is-constant-prop-trail-Undirected-Graph :
     {x y : vertex-Undirected-Graph G} →
     trail-Undirected-Graph x y → Prop lzero
-  is-constant-trail-Undirected-Graph-Prop t =
-    is-constant-walk-Undirected-Graph-Prop G (walk-trail-Undirected-Graph t)
+  is-constant-prop-trail-Undirected-Graph t =
+    is-constant-prop-walk-Undirected-Graph G (walk-trail-Undirected-Graph t)
 
   is-constant-trail-Undirected-Graph :
     {x y : vertex-Undirected-Graph G} → trail-Undirected-Graph x y → UU lzero
diff --git a/src/graph-theory/undirected-core-directed-graphs.lagda.md b/src/graph-theory/undirected-core-directed-graphs.lagda.md
new file mode 100644
index 0000000000..6d7760c8d8
--- /dev/null
+++ b/src/graph-theory/undirected-core-directed-graphs.lagda.md
@@ -0,0 +1,83 @@
+# The undirected core of a directed graph
+
+```agda
+module graph-theory.undirected-core-directed-graphs where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.symmetric-binary-relations
+open import foundation.symmetric-cores-binary-relations
+open import foundation.universe-levels
+
+open import graph-theory.directed-graphs
+open import graph-theory.forgetful-functor-from-undirected-graphs-to-directed-graphs
+open import graph-theory.morphisms-directed-graphs
+open import graph-theory.undirected-graphs
+```
+
+</details>
+
+## Idea
+
+The **undirected core** of a [directed graph](graph-theory.directed-graphs.md)
+`G` is the universal [undirected graph](graph-theory.undirected-graphs.md)
+`undirected-core G` equipped with a
+[morphism of directed graphs](graph-theory.morphisms-directed-graphs.md)
+
+```text
+  undirected-core G → G.
+```
+
+## Definitions
+
+### The undirected core of a directed graph
+
+```agda
+module _
+  {l1 l2 : Level} (G : Directed-Graph l1 l2)
+  where
+
+  vertex-undirected-core-Directed-Graph : UU l1
+  vertex-undirected-core-Directed-Graph = vertex-Directed-Graph G
+
+  edge-undirected-core-Directed-Graph :
+    Symmetric-Relation l2 vertex-undirected-core-Directed-Graph
+  edge-undirected-core-Directed-Graph =
+    symmetric-core-Relation (edge-Directed-Graph G)
+
+  undirected-core-Directed-Graph : Undirected-Graph l1 l2
+  pr1 undirected-core-Directed-Graph = vertex-undirected-core-Directed-Graph
+  pr2 undirected-core-Directed-Graph = edge-undirected-core-Directed-Graph
+```
+
+### The counit of the undirected core of a directed graph
+
+```agda
+module _
+  {l1 l2 : Level} (G : Directed-Graph l1 l2)
+  where
+
+  vertex-counit-undirected-core-Directed-Graph :
+    vertex-undirected-core-Directed-Graph G → vertex-Directed-Graph G
+  vertex-counit-undirected-core-Directed-Graph = id
+
+  edge-counit-undirected-core-Directed-Graph :
+    {x y : vertex-Directed-Graph G} →
+    edge-graph-Undirected-Graph (undirected-core-Directed-Graph G) x y →
+    edge-Directed-Graph G x y
+  edge-counit-undirected-core-Directed-Graph =
+    counit-symmetric-core-Relation (edge-Directed-Graph G)
+
+  counit-undirected-core-Directed-Graph :
+    hom-Directed-Graph
+      ( graph-Undirected-Graph (undirected-core-Directed-Graph G))
+      ( G)
+  pr1 counit-undirected-core-Directed-Graph =
+    vertex-counit-undirected-core-Directed-Graph
+  pr2 counit-undirected-core-Directed-Graph x y =
+    edge-counit-undirected-core-Directed-Graph
+```
diff --git a/src/graph-theory/undirected-graphs.lagda.md b/src/graph-theory/undirected-graphs.lagda.md
index c68110f024..56ddd1af42 100644
--- a/src/graph-theory/undirected-graphs.lagda.md
+++ b/src/graph-theory/undirected-graphs.lagda.md
@@ -9,7 +9,12 @@ module graph-theory.undirected-graphs where
 ```agda
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
+open import foundation.equivalence-extensionality
 open import foundation.equivalences
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.symmetric-binary-relations
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 open import foundation.unordered-pairs
@@ -21,14 +26,23 @@ open import graph-theory.directed-graphs
 
 ## Idea
 
-An **undirected graph** consists of a type `V` of vertices and a family `E` of
-types over the [unordered pairs](foundation.unordered-pairs.md) of `V`.
+An **undirected graph** consists of a type `V` of **vertices** and a
+[symmetric binary relation](foundation.symmetric-binary-relations.md) `E` edges.
 
-## Definition
+Note that in `agda-unimath`, symmetric binary relations on a type `V` are
+families of types over the [unordered pairs](foundation.unordered-pairs.md) of
+`V`. In other words, the edge relation of an undirected graph is assumed to be
+fully coherently symmetric. Furthermore, there may be multiple edges between
+vertices in an undirected graph, and undirected graphs may contain loops, i.e.,
+edges from a vertex to itself.
+
+## Definitions
+
+### Undirected graphs
 
 ```agda
 Undirected-Graph : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
-Undirected-Graph l1 l2 = Σ (UU l1) (λ V → unordered-pair V → UU l2)
+Undirected-Graph l1 l2 = Σ (UU l1) (Symmetric-Relation l2)
 
 module _
   {l1 l2 : Level} (G : Undirected-Graph l1 l2)
@@ -50,70 +64,52 @@ module _
     type-unordered-pair-vertices-Undirected-Graph p → vertex-Undirected-Graph
   element-unordered-pair-vertices-Undirected-Graph p = element-unordered-pair p
 
-  edge-Undirected-Graph : unordered-pair-vertices-Undirected-Graph → UU l2
+  edge-Undirected-Graph : Symmetric-Relation l2 vertex-Undirected-Graph
   edge-Undirected-Graph = pr2 G
 
   total-edge-Undirected-Graph : UU (lsuc lzero ⊔ l1 ⊔ l2)
   total-edge-Undirected-Graph =
     Σ unordered-pair-vertices-Undirected-Graph edge-Undirected-Graph
-```
-
-### The forgetful functor from directed graphs to undirected graphs
-
-```agda
-module _
-  {l1 l2 : Level} (G : Directed-Graph l1 l2)
-  where
-
-  undirected-graph-Graph : Undirected-Graph l1 l2
-  pr1 undirected-graph-Graph = vertex-Directed-Graph G
-  pr2 undirected-graph-Graph p =
-    Σ ( type-unordered-pair p)
-      ( λ x →
-        Σ ( type-unordered-pair p)
-          ( λ y →
-            edge-Directed-Graph G
-              ( element-unordered-pair p x)
-              ( element-unordered-pair p y)))
-
-module _
-  {l1 l2 : Level} (G : Undirected-Graph l1 l2)
-  where
-
-  graph-Undirected-Graph : Directed-Graph l1 (lsuc lzero ⊔ l1 ⊔ l2)
-  pr1 graph-Undirected-Graph = vertex-Undirected-Graph G
-  pr2 graph-Undirected-Graph x y =
-    Σ ( unordered-pair-vertices-Undirected-Graph G)
-      ( λ p →
-        ( mere-Eq-unordered-pair (standard-unordered-pair x y) p) ×
-        ( edge-Undirected-Graph G p))
-
-  graph-Undirected-Graph' : Directed-Graph l1 l2
-  pr1 graph-Undirected-Graph' = vertex-Undirected-Graph G
-  pr2 graph-Undirected-Graph' x y =
-    edge-Undirected-Graph G (standard-unordered-pair x y)
-```
-
-### Transporting edges along equalities of unordered pairs of vertices
-
-```agda
-module _
-  {l1 l2 : Level} (G : Undirected-Graph l1 l2)
-  where
 
-  equiv-tr-edge-Undirected-Graph :
-    (p q : unordered-pair-vertices-Undirected-Graph G)
-    (α : Eq-unordered-pair p q) →
-    edge-Undirected-Graph G p ≃ edge-Undirected-Graph G q
-  equiv-tr-edge-Undirected-Graph p q α =
-    equiv-tr (edge-Undirected-Graph G) (eq-Eq-unordered-pair' p q α)
-
-  tr-edge-Undirected-Graph :
-    (p q : unordered-pair-vertices-Undirected-Graph G)
-    (α : Eq-unordered-pair p q) →
-    edge-Undirected-Graph G p → edge-Undirected-Graph G q
-  tr-edge-Undirected-Graph p q α =
-    tr (edge-Undirected-Graph G) (eq-Eq-unordered-pair' p q α)
+  abstract
+    equiv-tr-edge-Undirected-Graph :
+      (p q : unordered-pair-vertices-Undirected-Graph) →
+      Eq-unordered-pair p q → edge-Undirected-Graph p ≃ edge-Undirected-Graph q
+    equiv-tr-edge-Undirected-Graph =
+      equiv-tr-Symmetric-Relation edge-Undirected-Graph
+
+    compute-refl-equiv-tr-edge-Undirected-Graph :
+      (p : unordered-pair-vertices-Undirected-Graph) →
+      equiv-tr-edge-Undirected-Graph p p (refl-Eq-unordered-pair p) ＝ id-equiv
+    compute-refl-equiv-tr-edge-Undirected-Graph =
+      compute-refl-equiv-tr-Symmetric-Relation edge-Undirected-Graph
+
+    htpy-compute-refl-equiv-tr-edge-Undirected-Graph :
+      (p : unordered-pair-vertices-Undirected-Graph) →
+      htpy-equiv
+        ( equiv-tr-edge-Undirected-Graph p p (refl-Eq-unordered-pair p))
+        ( id-equiv)
+    htpy-compute-refl-equiv-tr-edge-Undirected-Graph =
+      htpy-compute-refl-equiv-tr-Symmetric-Relation edge-Undirected-Graph
+
+  abstract
+    tr-edge-Undirected-Graph :
+      (p q : unordered-pair-vertices-Undirected-Graph) →
+      Eq-unordered-pair p q → edge-Undirected-Graph p → edge-Undirected-Graph q
+    tr-edge-Undirected-Graph =
+      tr-Symmetric-Relation edge-Undirected-Graph
+
+    compute-refl-tr-edge-Undirected-Graph :
+      (p : unordered-pair-vertices-Undirected-Graph) →
+      tr-edge-Undirected-Graph p p (refl-Eq-unordered-pair p) ＝ id
+    compute-refl-tr-edge-Undirected-Graph =
+      compute-refl-tr-Symmetric-Relation edge-Undirected-Graph
+
+    htpy-compute-refl-tr-edge-Undirected-Graph :
+      (p : unordered-pair-vertices-Undirected-Graph) →
+      tr-edge-Undirected-Graph p p (refl-Eq-unordered-pair p) ~ id
+    htpy-compute-refl-tr-edge-Undirected-Graph =
+      htpy-compute-refl-tr-Symmetric-Relation edge-Undirected-Graph
 ```
 
 ## External links
diff --git a/src/graph-theory/walks-directed-graphs.lagda.md b/src/graph-theory/walks-directed-graphs.lagda.md
index cd6f407532..3944b09790 100644
--- a/src/graph-theory/walks-directed-graphs.lagda.md
+++ b/src/graph-theory/walks-directed-graphs.lagda.md
@@ -111,6 +111,91 @@ module _
     snoc-walk-Directed-Graph' (cons-walk-Directed-Graph' e w) f
 ```
 
+### Vertices on a walk
+
+```agda
+module _
+  {l1 l2 : Level} (G : Directed-Graph l1 l2)
+  where
+
+  is-vertex-on-walk-Directed-Graph :
+    {x y : vertex-Directed-Graph G}
+    (w : walk-Directed-Graph G x y) (v : vertex-Directed-Graph G) → UU l1
+  is-vertex-on-walk-Directed-Graph {x} refl-walk-Directed-Graph v = v ＝ x
+  is-vertex-on-walk-Directed-Graph {x} (cons-walk-Directed-Graph e w) v =
+    ( v ＝ x) +
+    ( is-vertex-on-walk-Directed-Graph w v)
+
+  vertex-on-walk-Directed-Graph :
+    {x y : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y) → UU l1
+  vertex-on-walk-Directed-Graph w =
+    Σ (vertex-Directed-Graph G) (is-vertex-on-walk-Directed-Graph w)
+
+  vertex-vertex-on-walk-Directed-Graph :
+    {x y : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y) →
+    vertex-on-walk-Directed-Graph w → vertex-Directed-Graph G
+  vertex-vertex-on-walk-Directed-Graph w = pr1
+```
+
+### Edges on a walk
+
+```agda
+module _
+  {l1 l2 : Level} (G : Directed-Graph l1 l2)
+  where
+
+  data is-edge-on-walk-Directed-Graph :
+    {x y : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y)
+    {u v : vertex-Directed-Graph G} → edge-Directed-Graph G u v → UU (l1 ⊔ l2)
+    where
+    edge-is-edge-on-walk-Directed-Graph :
+      {x y z : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y)
+      (w : walk-Directed-Graph G y z) →
+      is-edge-on-walk-Directed-Graph (cons-walk-Directed-Graph e w) e
+    cons-is-edge-on-walk-Directed-Graph :
+      {x y z : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y)
+      (w : walk-Directed-Graph G y z) →
+      {u v : vertex-Directed-Graph G} (f : edge-Directed-Graph G u v) →
+      is-edge-on-walk-Directed-Graph w f →
+      is-edge-on-walk-Directed-Graph (cons-walk-Directed-Graph e w) f
+
+  edge-on-walk-Directed-Graph :
+    {x y : vertex-Directed-Graph G}
+    (w : walk-Directed-Graph G x y) → UU (l1 ⊔ l2)
+  edge-on-walk-Directed-Graph w =
+    Σ ( total-edge-Directed-Graph G)
+      ( λ e →
+        is-edge-on-walk-Directed-Graph w (edge-total-edge-Directed-Graph G e))
+
+  module _
+    {x y : vertex-Directed-Graph G}
+    (w : walk-Directed-Graph G x y)
+    (e : edge-on-walk-Directed-Graph w)
+    where
+
+    total-edge-edge-on-walk-Directed-Graph : total-edge-Directed-Graph G
+    total-edge-edge-on-walk-Directed-Graph = pr1 e
+
+    source-edge-on-walk-Directed-Graph : vertex-Directed-Graph G
+    source-edge-on-walk-Directed-Graph =
+      source-total-edge-Directed-Graph G total-edge-edge-on-walk-Directed-Graph
+
+    target-edge-on-walk-Directed-Graph : vertex-Directed-Graph G
+    target-edge-on-walk-Directed-Graph =
+      target-total-edge-Directed-Graph G total-edge-edge-on-walk-Directed-Graph
+
+    edge-edge-on-walk-Directed-Graph :
+      edge-Directed-Graph G
+        source-edge-on-walk-Directed-Graph
+        target-edge-on-walk-Directed-Graph
+    edge-edge-on-walk-Directed-Graph =
+      edge-total-edge-Directed-Graph G total-edge-edge-on-walk-Directed-Graph
+
+    is-edge-on-walk-edge-on-walk-Directed-Graph :
+      is-edge-on-walk-Directed-Graph w edge-edge-on-walk-Directed-Graph
+    is-edge-on-walk-edge-on-walk-Directed-Graph = pr2 e
+```
+
 ### The length of a walk in `G`
 
 ```agda
@@ -227,6 +312,168 @@ module _
     cons-walk-Directed-Graph e (concat-walk-Directed-Graph u v)
 ```
 
+### The action on walks of graph homomorphisms
+
+```agda
+walk-hom-Directed-Graph :
+  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
+  (f : hom-Directed-Graph G H) {x y : vertex-Directed-Graph G} →
+  walk-Directed-Graph G x y →
+  walk-Directed-Graph H
+    ( vertex-hom-Directed-Graph G H f x)
+    ( vertex-hom-Directed-Graph G H f y)
+walk-hom-Directed-Graph G H f refl-walk-Directed-Graph =
+  refl-walk-Directed-Graph
+walk-hom-Directed-Graph G H f (cons-walk-Directed-Graph e w) =
+  cons-walk-Directed-Graph
+    ( edge-hom-Directed-Graph G H f e)
+    ( walk-hom-Directed-Graph G H f w)
+```
+
+### The action on walks of length `n` of graph homomorphisms
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
+  (f : hom-Directed-Graph G H)
+  where
+
+  walk-of-length-hom-Directed-Graph :
+    (n : ℕ) {x y : vertex-Directed-Graph G} →
+    walk-of-length-Directed-Graph G n x y →
+    walk-of-length-Directed-Graph H n
+      ( vertex-hom-Directed-Graph G H f x)
+      ( vertex-hom-Directed-Graph G H f y)
+  walk-of-length-hom-Directed-Graph zero-ℕ {x} {y} (map-raise p) =
+    map-raise (ap (vertex-hom-Directed-Graph G H f) p)
+  walk-of-length-hom-Directed-Graph (succ-ℕ n) =
+    map-Σ
+      ( λ z →
+        ( edge-Directed-Graph H (vertex-hom-Directed-Graph G H f _) z) ×
+        ( walk-of-length-Directed-Graph H n z
+          ( vertex-hom-Directed-Graph G H f _)))
+      ( vertex-hom-Directed-Graph G H f)
+      ( λ z →
+        map-prod
+          ( edge-hom-Directed-Graph G H f)
+          ( walk-of-length-hom-Directed-Graph n))
+
+  square-compute-total-walk-of-length-hom-Directed-Graph :
+    (x y : vertex-Directed-Graph G) →
+    coherence-square-maps
+      ( tot (λ n → walk-of-length-hom-Directed-Graph n {x} {y}))
+      ( map-compute-total-walk-of-length-Directed-Graph G x y)
+      ( map-compute-total-walk-of-length-Directed-Graph H
+        ( vertex-hom-Directed-Graph G H f x)
+        ( vertex-hom-Directed-Graph G H f y))
+      ( walk-hom-Directed-Graph G H f {x} {y})
+  square-compute-total-walk-of-length-hom-Directed-Graph
+    x .x (zero-ℕ , map-raise refl) = refl
+  square-compute-total-walk-of-length-hom-Directed-Graph
+    x y (succ-ℕ n , z , e , w) =
+    ap
+      ( cons-walk-Directed-Graph (edge-hom-Directed-Graph G H f e))
+      ( square-compute-total-walk-of-length-hom-Directed-Graph z y (n , w))
+```
+
+### The action on walks of length `n` of equivalences of graphs
+
+```agda
+equiv-walk-of-length-equiv-Directed-Graph :
+  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
+  (f : equiv-Directed-Graph G H) (n : ℕ) {x y : vertex-Directed-Graph G} →
+  walk-of-length-Directed-Graph G n x y ≃
+  walk-of-length-Directed-Graph H n
+    ( vertex-equiv-Directed-Graph G H f x)
+    ( vertex-equiv-Directed-Graph G H f y)
+equiv-walk-of-length-equiv-Directed-Graph G H f zero-ℕ =
+  equiv-raise _ _
+    ( equiv-ap (equiv-vertex-equiv-Directed-Graph G H f) _ _)
+equiv-walk-of-length-equiv-Directed-Graph G H f (succ-ℕ n) =
+  equiv-Σ
+    ( λ z →
+      ( edge-Directed-Graph H (vertex-equiv-Directed-Graph G H f _) z) ×
+      ( walk-of-length-Directed-Graph H n z
+        ( vertex-equiv-Directed-Graph G H f _)))
+    ( equiv-vertex-equiv-Directed-Graph G H f)
+    ( λ z →
+      equiv-prod
+        ( equiv-edge-equiv-Directed-Graph G H f _ _)
+        ( equiv-walk-of-length-equiv-Directed-Graph G H f n))
+```
+
+### The action of equivalences on walks
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
+  (e : equiv-Directed-Graph G H)
+  where
+
+  walk-equiv-Directed-Graph :
+    {x y : vertex-Directed-Graph G} →
+    walk-Directed-Graph G x y →
+    walk-Directed-Graph H
+      ( vertex-equiv-Directed-Graph G H e x)
+      ( vertex-equiv-Directed-Graph G H e y)
+  walk-equiv-Directed-Graph =
+    walk-hom-Directed-Graph G H (hom-equiv-Directed-Graph G H e)
+
+  square-compute-total-walk-of-length-equiv-Directed-Graph :
+    (x y : vertex-Directed-Graph G) →
+    coherence-square-maps
+      ( tot
+        ( λ n →
+          map-equiv
+            ( equiv-walk-of-length-equiv-Directed-Graph G H e n {x} {y})))
+      ( map-compute-total-walk-of-length-Directed-Graph G x y)
+      ( map-compute-total-walk-of-length-Directed-Graph H
+        ( vertex-equiv-Directed-Graph G H e x)
+        ( vertex-equiv-Directed-Graph G H e y))
+      ( walk-equiv-Directed-Graph {x} {y})
+  square-compute-total-walk-of-length-equiv-Directed-Graph
+    x .x (zero-ℕ , map-raise refl) = refl
+  square-compute-total-walk-of-length-equiv-Directed-Graph
+    x y (succ-ℕ n , z , f , w) =
+    ap
+      ( cons-walk-Directed-Graph (edge-equiv-Directed-Graph G H e x z f))
+      ( square-compute-total-walk-of-length-equiv-Directed-Graph z y (n , w))
+
+  is-equiv-walk-equiv-Directed-Graph :
+    {x y : vertex-Directed-Graph G} →
+    is-equiv (walk-equiv-Directed-Graph {x} {y})
+  is-equiv-walk-equiv-Directed-Graph {x} {y} =
+    is-equiv-right-is-equiv-left-square
+      ( map-equiv
+        ( equiv-tot
+        ( λ n → equiv-walk-of-length-equiv-Directed-Graph G H e n {x} {y})))
+      ( walk-equiv-Directed-Graph {x} {y})
+      ( map-compute-total-walk-of-length-Directed-Graph G x y)
+      ( map-compute-total-walk-of-length-Directed-Graph H
+        ( vertex-equiv-Directed-Graph G H e x)
+        ( vertex-equiv-Directed-Graph G H e y))
+      ( inv-htpy
+        ( square-compute-total-walk-of-length-equiv-Directed-Graph x y))
+      ( is-equiv-map-compute-total-walk-of-length-Directed-Graph G x y)
+      ( is-equiv-map-compute-total-walk-of-length-Directed-Graph H
+        ( vertex-equiv-Directed-Graph G H e x)
+        ( vertex-equiv-Directed-Graph G H e y))
+      ( is-equiv-map-equiv
+        ( equiv-tot
+          ( λ n → equiv-walk-of-length-equiv-Directed-Graph G H e n)))
+
+  equiv-walk-equiv-Directed-Graph :
+    {x y : vertex-Directed-Graph G} →
+    walk-Directed-Graph G x y ≃
+    walk-Directed-Graph H
+      ( vertex-equiv-Directed-Graph G H e x)
+      ( vertex-equiv-Directed-Graph G H e y)
+  pr1 (equiv-walk-equiv-Directed-Graph {x} {y}) =
+    walk-equiv-Directed-Graph
+  pr2 (equiv-walk-equiv-Directed-Graph {x} {y}) =
+    is-equiv-walk-equiv-Directed-Graph
+```
+
 ## Properties
 
 ### The two dual definitions of walks are equivalent
@@ -441,253 +688,6 @@ module _
     refl
 ```
 
-### Vertices on a walk
-
-```agda
-module _
-  {l1 l2 : Level} (G : Directed-Graph l1 l2)
-  where
-
-  is-vertex-on-walk-Directed-Graph :
-    {x y : vertex-Directed-Graph G}
-    (w : walk-Directed-Graph G x y) (v : vertex-Directed-Graph G) → UU l1
-  is-vertex-on-walk-Directed-Graph {x} refl-walk-Directed-Graph v = v ＝ x
-  is-vertex-on-walk-Directed-Graph {x} (cons-walk-Directed-Graph e w) v =
-    ( v ＝ x) +
-    ( is-vertex-on-walk-Directed-Graph w v)
-
-  vertex-on-walk-Directed-Graph :
-    {x y : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y) → UU l1
-  vertex-on-walk-Directed-Graph w =
-    Σ (vertex-Directed-Graph G) (is-vertex-on-walk-Directed-Graph w)
-
-  vertex-vertex-on-walk-Directed-Graph :
-    {x y : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y) →
-    vertex-on-walk-Directed-Graph w → vertex-Directed-Graph G
-  vertex-vertex-on-walk-Directed-Graph w = pr1
-```
-
-### Edges on a walk
-
-```agda
-module _
-  {l1 l2 : Level} (G : Directed-Graph l1 l2)
-  where
-
-  data is-edge-on-walk-Directed-Graph :
-    {x y : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y)
-    {u v : vertex-Directed-Graph G} → edge-Directed-Graph G u v → UU (l1 ⊔ l2)
-    where
-    edge-is-edge-on-walk-Directed-Graph :
-      {x y z : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y)
-      (w : walk-Directed-Graph G y z) →
-      is-edge-on-walk-Directed-Graph (cons-walk-Directed-Graph e w) e
-    cons-is-edge-on-walk-Directed-Graph :
-      {x y z : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y)
-      (w : walk-Directed-Graph G y z) →
-      {u v : vertex-Directed-Graph G} (f : edge-Directed-Graph G u v) →
-      is-edge-on-walk-Directed-Graph w f →
-      is-edge-on-walk-Directed-Graph (cons-walk-Directed-Graph e w) f
-
-  edge-on-walk-Directed-Graph :
-    {x y : vertex-Directed-Graph G}
-    (w : walk-Directed-Graph G x y) → UU (l1 ⊔ l2)
-  edge-on-walk-Directed-Graph w =
-    Σ ( total-edge-Directed-Graph G)
-      ( λ e →
-        is-edge-on-walk-Directed-Graph w (edge-total-edge-Directed-Graph G e))
-
-  module _
-    {x y : vertex-Directed-Graph G}
-    (w : walk-Directed-Graph G x y)
-    (e : edge-on-walk-Directed-Graph w)
-    where
-
-    total-edge-edge-on-walk-Directed-Graph : total-edge-Directed-Graph G
-    total-edge-edge-on-walk-Directed-Graph = pr1 e
-
-    source-edge-on-walk-Directed-Graph : vertex-Directed-Graph G
-    source-edge-on-walk-Directed-Graph =
-      source-total-edge-Directed-Graph G total-edge-edge-on-walk-Directed-Graph
-
-    target-edge-on-walk-Directed-Graph : vertex-Directed-Graph G
-    target-edge-on-walk-Directed-Graph =
-      target-total-edge-Directed-Graph G total-edge-edge-on-walk-Directed-Graph
-
-    edge-edge-on-walk-Directed-Graph :
-      edge-Directed-Graph G
-        source-edge-on-walk-Directed-Graph
-        target-edge-on-walk-Directed-Graph
-    edge-edge-on-walk-Directed-Graph =
-      edge-total-edge-Directed-Graph G total-edge-edge-on-walk-Directed-Graph
-
-    is-edge-on-walk-edge-on-walk-Directed-Graph :
-      is-edge-on-walk-Directed-Graph w edge-edge-on-walk-Directed-Graph
-    is-edge-on-walk-edge-on-walk-Directed-Graph = pr2 e
-```
-
-### The action on walks of graph homomorphisms
-
-```agda
-walk-hom-Directed-Graph :
-  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
-  (f : hom-Directed-Graph G H) {x y : vertex-Directed-Graph G} →
-  walk-Directed-Graph G x y →
-  walk-Directed-Graph H
-    ( vertex-hom-Directed-Graph G H f x)
-    ( vertex-hom-Directed-Graph G H f y)
-walk-hom-Directed-Graph G H f refl-walk-Directed-Graph =
-  refl-walk-Directed-Graph
-walk-hom-Directed-Graph G H f (cons-walk-Directed-Graph e w) =
-  cons-walk-Directed-Graph
-    ( edge-hom-Directed-Graph G H f e)
-    ( walk-hom-Directed-Graph G H f w)
-```
-
-### The action on walks of length `n` of graph homomorphisms
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
-  (f : hom-Directed-Graph G H)
-  where
-
-  walk-of-length-hom-Directed-Graph :
-    (n : ℕ) {x y : vertex-Directed-Graph G} →
-    walk-of-length-Directed-Graph G n x y →
-    walk-of-length-Directed-Graph H n
-    ( vertex-hom-Directed-Graph G H f x)
-    ( vertex-hom-Directed-Graph G H f y)
-  walk-of-length-hom-Directed-Graph zero-ℕ {x} {y} (map-raise p) =
-    map-raise (ap (vertex-hom-Directed-Graph G H f) p)
-  walk-of-length-hom-Directed-Graph (succ-ℕ n) =
-    map-Σ
-      ( λ z →
-        ( edge-Directed-Graph H (vertex-hom-Directed-Graph G H f _) z) ×
-        ( walk-of-length-Directed-Graph H n z
-          ( vertex-hom-Directed-Graph G H f _)))
-      ( vertex-hom-Directed-Graph G H f)
-      ( λ z →
-        map-prod
-          ( edge-hom-Directed-Graph G H f)
-          ( walk-of-length-hom-Directed-Graph n))
-
-  square-compute-total-walk-of-length-hom-Directed-Graph :
-    (x y : vertex-Directed-Graph G) →
-    coherence-square-maps
-      ( tot (λ n → walk-of-length-hom-Directed-Graph n {x} {y}))
-      ( map-compute-total-walk-of-length-Directed-Graph G x y)
-      ( map-compute-total-walk-of-length-Directed-Graph H
-        ( vertex-hom-Directed-Graph G H f x)
-        ( vertex-hom-Directed-Graph G H f y))
-      ( walk-hom-Directed-Graph G H f {x} {y})
-  square-compute-total-walk-of-length-hom-Directed-Graph
-    x .x (zero-ℕ , map-raise refl) = refl
-  square-compute-total-walk-of-length-hom-Directed-Graph
-    x y (succ-ℕ n , z , e , w) =
-    ap
-      ( cons-walk-Directed-Graph (edge-hom-Directed-Graph G H f e))
-      ( square-compute-total-walk-of-length-hom-Directed-Graph z y (n , w))
-```
-
-### The action on walks of length `n` of equivalences of graphs
-
-```agda
-equiv-walk-of-length-equiv-Directed-Graph :
-  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
-  (f : equiv-Directed-Graph G H) (n : ℕ) {x y : vertex-Directed-Graph G} →
-  walk-of-length-Directed-Graph G n x y ≃
-  walk-of-length-Directed-Graph H n
-    ( vertex-equiv-Directed-Graph G H f x)
-    ( vertex-equiv-Directed-Graph G H f y)
-equiv-walk-of-length-equiv-Directed-Graph G H f zero-ℕ =
-  equiv-raise _ _
-    ( equiv-ap (equiv-vertex-equiv-Directed-Graph G H f) _ _)
-equiv-walk-of-length-equiv-Directed-Graph G H f (succ-ℕ n) =
-  equiv-Σ
-    ( λ z →
-      ( edge-Directed-Graph H (vertex-equiv-Directed-Graph G H f _) z) ×
-      ( walk-of-length-Directed-Graph H n z
-        ( vertex-equiv-Directed-Graph G H f _)))
-    ( equiv-vertex-equiv-Directed-Graph G H f)
-    ( λ z →
-      equiv-prod
-        ( equiv-edge-equiv-Directed-Graph G H f _ _)
-        ( equiv-walk-of-length-equiv-Directed-Graph G H f n))
-```
-
-### The action of equivalences on walks
-
-```agda
-module _
-  {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4)
-  (e : equiv-Directed-Graph G H)
-  where
-
-  walk-equiv-Directed-Graph :
-    {x y : vertex-Directed-Graph G} →
-    walk-Directed-Graph G x y →
-    walk-Directed-Graph H
-      ( vertex-equiv-Directed-Graph G H e x)
-      ( vertex-equiv-Directed-Graph G H e y)
-  walk-equiv-Directed-Graph =
-    walk-hom-Directed-Graph G H (hom-equiv-Directed-Graph G H e)
-
-  square-compute-total-walk-of-length-equiv-Directed-Graph :
-    (x y : vertex-Directed-Graph G) →
-    coherence-square-maps
-      ( tot
-        ( λ n →
-          map-equiv
-            ( equiv-walk-of-length-equiv-Directed-Graph G H e n {x} {y})))
-      ( map-compute-total-walk-of-length-Directed-Graph G x y)
-      ( map-compute-total-walk-of-length-Directed-Graph H
-        ( vertex-equiv-Directed-Graph G H e x)
-        ( vertex-equiv-Directed-Graph G H e y))
-      ( walk-equiv-Directed-Graph {x} {y})
-  square-compute-total-walk-of-length-equiv-Directed-Graph
-    x .x (zero-ℕ , map-raise refl) = refl
-  square-compute-total-walk-of-length-equiv-Directed-Graph
-    x y (succ-ℕ n , z , f , w) =
-    ap
-      ( cons-walk-Directed-Graph (edge-equiv-Directed-Graph G H e x z f))
-      ( square-compute-total-walk-of-length-equiv-Directed-Graph z y (n , w))
-
-  is-equiv-walk-equiv-Directed-Graph :
-    {x y : vertex-Directed-Graph G} →
-    is-equiv (walk-equiv-Directed-Graph {x} {y})
-  is-equiv-walk-equiv-Directed-Graph {x} {y} =
-    is-equiv-right-is-equiv-left-square
-      ( map-equiv
-        ( equiv-tot
-        ( λ n → equiv-walk-of-length-equiv-Directed-Graph G H e n {x} {y})))
-      ( walk-equiv-Directed-Graph {x} {y})
-      ( map-compute-total-walk-of-length-Directed-Graph G x y)
-      ( map-compute-total-walk-of-length-Directed-Graph H
-        ( vertex-equiv-Directed-Graph G H e x)
-        ( vertex-equiv-Directed-Graph G H e y))
-      ( inv-htpy
-        ( square-compute-total-walk-of-length-equiv-Directed-Graph x y))
-      ( is-equiv-map-compute-total-walk-of-length-Directed-Graph G x y)
-      ( is-equiv-map-compute-total-walk-of-length-Directed-Graph H
-        ( vertex-equiv-Directed-Graph G H e x)
-        ( vertex-equiv-Directed-Graph G H e y))
-      ( is-equiv-map-equiv
-        ( equiv-tot
-          ( λ n → equiv-walk-of-length-equiv-Directed-Graph G H e n)))
-
-  equiv-walk-equiv-Directed-Graph :
-    {x y : vertex-Directed-Graph G} →
-    walk-Directed-Graph G x y ≃
-    walk-Directed-Graph H
-      ( vertex-equiv-Directed-Graph G H e x)
-      ( vertex-equiv-Directed-Graph G H e y)
-  pr1 (equiv-walk-equiv-Directed-Graph {x} {y}) =
-    walk-equiv-Directed-Graph
-  pr2 (equiv-walk-equiv-Directed-Graph {x} {y}) =
-    is-equiv-walk-equiv-Directed-Graph
-```
-
 ### If `concat-walk-Directed-Graph u v ＝ refl-walk-Directed-Graph` then both `u` and `v` are `refl-walk-Directed-Graph`
 
 ```agda
diff --git a/src/graph-theory/walks-finite-undirected-graphs.lagda.md b/src/graph-theory/walks-finite-undirected-graphs.lagda.md
new file mode 100644
index 0000000000..3909cdd9d0
--- /dev/null
+++ b/src/graph-theory/walks-finite-undirected-graphs.lagda.md
@@ -0,0 +1,543 @@
+# Walks in finite undirected graphs
+
+```agda
+module graph-theory.walks-finite-undirected-graphs where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.equality-natural-numbers
+open import elementary-number-theory.natural-numbers
+
+open import foundation.contractible-types
+open import foundation.coproduct-types
+open import foundation.decidable-equality
+open import foundation.decidable-propositions
+open import foundation.decidable-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.torsorial-type-families
+open import foundation.universe-levels
+open import foundation.unordered-pairs
+
+open import graph-theory.finite-undirected-graphs
+open import graph-theory.walks-undirected-graphs
+
+open import univalent-combinatorics.standard-finite-types
+```
+
+</details>
+
+## Idea
+
+A **walk** in a
+[finite undirected graph](graph-theory.finite-undirected-graphs.md) `G` is
+simply a [walk](graph-theory.walks-undirected-graphs.md) in its underlying
+[undirected graph](graph-theory.undirected-graphs.md).
+
+Note that the type of walks in a finite undirected graph does not need to be
+[finite](univalent-combinatorics.finite-types.md), since edges can be repeated
+in walks. However, the type of walks from `x` to `y` in a finite undirected
+graph has [decidable equality](foundation.decidable-equality.md), and the type
+of walks of a given length `n` in a finite undirected graph is finite.
+
+## Definition
+
+### Walks in finite undirected graphs
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  where
+
+  walk-Undirected-Graph-𝔽 :
+    (x y : vertex-Undirected-Graph-𝔽 G) → UU (lsuc lzero ⊔ l1 ⊔ l2)
+  walk-Undirected-Graph-𝔽 =
+    walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### The vertices on a walk in a finite undirected graph
+
+```agda
+module _
+  {l1 l2 : Level}
+  (G : Undirected-Graph-𝔽 l1 l2) {x : vertex-Undirected-Graph-𝔽 G}
+  where
+
+  is-vertex-on-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y) →
+    vertex-Undirected-Graph-𝔽 G → UU l1
+  is-vertex-on-walk-Undirected-Graph-𝔽 =
+    is-vertex-on-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+
+  vertex-on-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G}
+    (w : walk-Undirected-Graph-𝔽 G x y) → UU l1
+  vertex-on-walk-Undirected-Graph-𝔽 =
+    vertex-on-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+
+  vertex-vertex-on-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y) →
+    vertex-on-walk-Undirected-Graph-𝔽 w → vertex-Undirected-Graph-𝔽 G
+  vertex-vertex-on-walk-Undirected-Graph-𝔽 =
+    vertex-vertex-on-walk-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### Edges on a walk
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  {x : vertex-Undirected-Graph-𝔽 G}
+  where
+
+  is-edge-on-walk-Undirected-Graph-𝔽' :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y) →
+    total-edge-Undirected-Graph-𝔽 G → UU (lsuc lzero ⊔ l1 ⊔ l2)
+  is-edge-on-walk-Undirected-Graph-𝔽' =
+    is-edge-on-walk-Undirected-Graph' (undirected-graph-Undirected-Graph-𝔽 G)
+
+  is-edge-on-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y) →
+    (p : unordered-pair-vertices-Undirected-Graph-𝔽 G) →
+    edge-Undirected-Graph-𝔽 G p → UU (lsuc lzero ⊔ l1 ⊔ l2)
+  is-edge-on-walk-Undirected-Graph-𝔽 =
+    is-edge-on-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+
+  edge-on-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y) →
+    UU (lsuc lzero ⊔ l1 ⊔ l2)
+  edge-on-walk-Undirected-Graph-𝔽 =
+    edge-on-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+
+  edge-edge-on-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G}
+    (w : walk-Undirected-Graph-𝔽 G x y) →
+    edge-on-walk-Undirected-Graph-𝔽 w → total-edge-Undirected-Graph-𝔽 G
+  edge-edge-on-walk-Undirected-Graph-𝔽 =
+    edge-edge-on-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### Concatenating walks
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  {x : vertex-Undirected-Graph-𝔽 G}
+  where
+
+  concat-walk-Undirected-Graph-𝔽 :
+    {y z : vertex-Undirected-Graph-𝔽 G} →
+    walk-Undirected-Graph-𝔽 G x y →
+    walk-Undirected-Graph-𝔽 G y z →
+    walk-Undirected-Graph-𝔽 G x z
+  concat-walk-Undirected-Graph-𝔽 =
+    concat-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### The length of a walk
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  {x : vertex-Undirected-Graph-𝔽 G}
+  where
+
+  length-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} → walk-Undirected-Graph-𝔽 G x y → ℕ
+  length-walk-Undirected-Graph-𝔽 =
+    length-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### Walks of a fixed length
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  where
+
+  walk-of-length-Undirected-Graph-𝔽 :
+    ℕ → (x y : vertex-Undirected-Graph-𝔽 G) → UU (lsuc lzero ⊔ l1 ⊔ l2)
+  walk-of-length-Undirected-Graph-𝔽 =
+    walk-of-length-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+
+  map-compute-total-walk-of-length-Undirected-Graph-𝔽 :
+    (x y : vertex-Undirected-Graph-𝔽 G) →
+    walk-Undirected-Graph-𝔽 G x y →
+    Σ ℕ (λ n → walk-of-length-Undirected-Graph-𝔽 n x y)
+  map-compute-total-walk-of-length-Undirected-Graph-𝔽 =
+    map-compute-total-walk-of-length-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+
+  map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 :
+    (x y : vertex-Undirected-Graph-𝔽 G) →
+    Σ ℕ (λ n → walk-of-length-Undirected-Graph-𝔽 n x y) →
+    walk-Undirected-Graph-𝔽 G x y
+  map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 =
+    map-inv-compute-total-walk-of-length-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+
+  is-section-map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 :
+    (x y : vertex-Undirected-Graph-𝔽 G) →
+    ( map-compute-total-walk-of-length-Undirected-Graph-𝔽 x y ∘
+      map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 x y) ~ id
+  is-section-map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 =
+    is-section-map-inv-compute-total-walk-of-length-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+
+  is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 :
+    (x y : vertex-Undirected-Graph-𝔽 G) →
+    ( map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 x y ∘
+      map-compute-total-walk-of-length-Undirected-Graph-𝔽 x y) ~ id
+  is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 =
+    is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+
+  is-equiv-map-compute-total-walk-of-length-Undirected-Graph-𝔽 :
+    (x y : vertex-Undirected-Graph-𝔽 G) →
+    is-equiv (map-compute-total-walk-of-length-Undirected-Graph-𝔽 x y)
+  is-equiv-map-compute-total-walk-of-length-Undirected-Graph-𝔽 =
+    is-equiv-map-compute-total-walk-of-length-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+
+  compute-total-walk-of-length-Undirected-Graph-𝔽 :
+    (x y : vertex-Undirected-Graph-𝔽 G) →
+    walk-Undirected-Graph-𝔽 G x y ≃
+    Σ ℕ (λ n → walk-of-length-Undirected-Graph-𝔽 n x y)
+  compute-total-walk-of-length-Undirected-Graph-𝔽 =
+    compute-total-walk-of-length-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+## Properties
+
+### The type of vertices on the constant walk is contractible
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  (x : vertex-Undirected-Graph-𝔽 G)
+  where
+
+  is-contr-vertex-on-refl-walk-Undirected-Graph-𝔽 :
+    is-contr
+      ( vertex-on-walk-Undirected-Graph-𝔽 G
+        ( refl-walk-Undirected-Graph {x = x}))
+  is-contr-vertex-on-refl-walk-Undirected-Graph-𝔽 =
+    is-contr-vertex-on-refl-walk-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+      ( x)
+```
+
+### The type of vertices on a walk is equivalent to `Fin (n + 1)` where `n` is the length of the walk
+
+```agda
+module _
+  {l1 l2 : Level}
+  (G : Undirected-Graph-𝔽 l1 l2)
+  {x : vertex-Undirected-Graph-𝔽 G}
+  where
+
+  compute-vertex-on-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y) →
+    vertex-on-walk-Undirected-Graph-𝔽 G w ≃
+    Fin (succ-ℕ (length-walk-Undirected-Graph-𝔽 G w))
+  compute-vertex-on-walk-Undirected-Graph-𝔽 =
+    compute-vertex-on-walk-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### The type of edges on a constant walk is empty
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  (x : vertex-Undirected-Graph-𝔽 G)
+  where
+
+  is-empty-edge-on-walk-refl-walk-Undirected-Graph-𝔽 :
+    is-empty
+      ( edge-on-walk-Undirected-Graph-𝔽 G
+        ( refl-walk-Undirected-Graph {x = x}))
+  is-empty-edge-on-walk-refl-walk-Undirected-Graph-𝔽 =
+    is-empty-edge-on-walk-refl-walk-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+      ( x)
+```
+
+### The type of edges on a walk is equivalent to `Fin n` where `n` is the length of the walk
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  {x : vertex-Undirected-Graph-𝔽 G}
+  where
+
+  compute-edge-on-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G}
+    (w : walk-Undirected-Graph-𝔽 G x y) →
+    edge-on-walk-Undirected-Graph-𝔽 G w ≃
+    Fin (length-walk-Undirected-Graph-𝔽 G w)
+  compute-edge-on-walk-Undirected-Graph-𝔽 =
+    compute-edge-on-walk-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### Right unit law for concatenation of walks
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  {x : vertex-Undirected-Graph-𝔽 G}
+  where
+
+  right-unit-law-concat-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G}
+    (w : walk-Undirected-Graph-𝔽 G x y) →
+    (concat-walk-Undirected-Graph-𝔽 G w refl-walk-Undirected-Graph) ＝ w
+  right-unit-law-concat-walk-Undirected-Graph-𝔽 =
+    right-unit-law-concat-walk-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### For any walk `w` from `x` to `y` and any vertex `v` on `w`, we can decompose `w` into a walk `w1` from `x` to `v` and a walk `w2` from `v` to `y`
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  {x : vertex-Undirected-Graph-𝔽 G}
+  where
+
+  first-segment-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y)
+    (v : vertex-on-walk-Undirected-Graph-𝔽 G w) →
+    walk-Undirected-Graph-𝔽 G x (vertex-vertex-on-walk-Undirected-Graph-𝔽 G w v)
+  first-segment-walk-Undirected-Graph-𝔽 =
+    first-segment-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+
+  second-segment-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y)
+    (v : vertex-on-walk-Undirected-Graph-𝔽 G w) →
+    walk-Undirected-Graph-𝔽 G (vertex-vertex-on-walk-Undirected-Graph-𝔽 G w v) y
+  second-segment-walk-Undirected-Graph-𝔽 =
+    second-segment-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+
+  eq-decompose-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y)
+    (v : vertex-on-walk-Undirected-Graph-𝔽 G w) →
+    ( concat-walk-Undirected-Graph-𝔽 G
+      ( first-segment-walk-Undirected-Graph-𝔽 w v)
+      ( second-segment-walk-Undirected-Graph-𝔽 w v)) ＝ w
+  eq-decompose-walk-Undirected-Graph-𝔽 =
+    eq-decompose-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### For any edge `e` on `p`, if `v` is a vertex on `w` then it is a vertex on `cons p e w`
+
+```agda
+is-vertex-on-walk-cons-walk-Undirected-Graph-𝔽 :
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  (p : unordered-pair-vertices-Undirected-Graph-𝔽 G)
+  (e : edge-Undirected-Graph-𝔽 G p) →
+  {x : vertex-Undirected-Graph-𝔽 G} {y : type-unordered-pair p} →
+  (w : walk-Undirected-Graph-𝔽 G x (element-unordered-pair p y)) →
+  {v : vertex-Undirected-Graph-𝔽 G} →
+  is-vertex-on-walk-Undirected-Graph-𝔽 G w v →
+  is-vertex-on-walk-Undirected-Graph-𝔽 G (cons-walk-Undirected-Graph p e w) v
+is-vertex-on-walk-cons-walk-Undirected-Graph-𝔽 G =
+  is-vertex-on-walk-cons-walk-Undirected-Graph
+    ( undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### For any decomposition of a walk `w` into `w1` followed by `w2`, any vertex on `w` is a vertex on `w1` or on `w2`
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  {x : vertex-Undirected-Graph-𝔽 G}
+  where
+
+  is-vertex-on-first-segment-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y) →
+    (v : vertex-on-walk-Undirected-Graph-𝔽 G w) →
+    vertex-Undirected-Graph-𝔽 G → UU l1
+  is-vertex-on-first-segment-walk-Undirected-Graph-𝔽 w v =
+    is-vertex-on-walk-Undirected-Graph-𝔽 G
+      ( first-segment-walk-Undirected-Graph-𝔽 G w v)
+
+  is-vertex-on-second-segment-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y) →
+    (v : vertex-on-walk-Undirected-Graph-𝔽 G w) →
+    vertex-Undirected-Graph-𝔽 G → UU l1
+  is-vertex-on-second-segment-walk-Undirected-Graph-𝔽 w v =
+    is-vertex-on-walk-Undirected-Graph-𝔽 G
+      ( second-segment-walk-Undirected-Graph-𝔽 G w v)
+
+  is-vertex-on-first-or-second-segment-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y) →
+    (u v : vertex-on-walk-Undirected-Graph-𝔽 G w) →
+    ( is-vertex-on-first-segment-walk-Undirected-Graph-𝔽 w u
+      ( vertex-vertex-on-walk-Undirected-Graph-𝔽 G w v)) +
+    ( is-vertex-on-second-segment-walk-Undirected-Graph-𝔽 w u
+      ( vertex-vertex-on-walk-Undirected-Graph-𝔽 G w v))
+  is-vertex-on-first-or-second-segment-walk-Undirected-Graph-𝔽 =
+    is-vertex-on-first-or-second-segment-walk-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### For any decomposition of a walk `w` into `w1` followed by `w2`, any vertex on `w1` is a vertex on `w`
+
+```agda
+is-vertex-on-walk-is-vertex-on-first-segment-walk-Undirected-Graph-𝔽 :
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  {x y : vertex-Undirected-Graph-𝔽 G}
+  (w : walk-Undirected-Graph-𝔽 G x y)
+  (v : vertex-on-walk-Undirected-Graph-𝔽 G w)
+  (u : vertex-Undirected-Graph-𝔽 G) →
+  is-vertex-on-first-segment-walk-Undirected-Graph-𝔽 G w v u →
+  is-vertex-on-walk-Undirected-Graph-𝔽 G w u
+is-vertex-on-walk-is-vertex-on-first-segment-walk-Undirected-Graph-𝔽 G =
+  is-vertex-on-walk-is-vertex-on-first-segment-walk-Undirected-Graph
+    ( undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### For any decomposition of a walk `w` into `w1` followed by `w2`, any vertex on `w2` is a vertex on `w`
+
+```agda
+is-vertex-on-walk-is-vertex-on-second-segment-walk-Undirected-Graph-𝔽 :
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  {x y : vertex-Undirected-Graph-𝔽 G}
+  (w : walk-Undirected-Graph-𝔽 G x y)
+  (v : vertex-on-walk-Undirected-Graph-𝔽 G w)
+  (u : vertex-Undirected-Graph-𝔽 G) →
+  is-vertex-on-second-segment-walk-Undirected-Graph-𝔽 G w v u →
+  is-vertex-on-walk-Undirected-Graph-𝔽 G w u
+is-vertex-on-walk-is-vertex-on-second-segment-walk-Undirected-Graph-𝔽 G =
+  is-vertex-on-walk-is-vertex-on-second-segment-walk-Undirected-Graph
+    ( undirected-graph-Undirected-Graph-𝔽 G)
+```
+
+### Constant walks are identifications
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  {x : vertex-Undirected-Graph-𝔽 G}
+  where
+
+  is-constant-walk-Undirected-Graph-𝔽-Prop :
+    {y : vertex-Undirected-Graph-𝔽 G} →
+    walk-Undirected-Graph-𝔽 G x y → Prop lzero
+  is-constant-walk-Undirected-Graph-𝔽-Prop =
+    is-constant-prop-walk-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+
+  is-constant-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} →
+    walk-Undirected-Graph-𝔽 G x y → UU lzero
+  is-constant-walk-Undirected-Graph-𝔽 =
+    is-constant-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+
+  constant-walk-Undirected-Graph-𝔽 :
+    (y : vertex-Undirected-Graph-𝔽 G) → UU (lsuc lzero ⊔ l1 ⊔ l2)
+  constant-walk-Undirected-Graph-𝔽 =
+    constant-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G) {x}
+
+  is-decidable-is-constant-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} (w : walk-Undirected-Graph-𝔽 G x y) →
+    is-decidable (is-constant-walk-Undirected-Graph-𝔽 w)
+  is-decidable-is-constant-walk-Undirected-Graph-𝔽 =
+    is-decidable-is-constant-walk-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+
+  refl-constant-walk-Undirected-Graph-𝔽 :
+    constant-walk-Undirected-Graph-𝔽 x
+  refl-constant-walk-Undirected-Graph-𝔽 =
+    refl-constant-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+
+  is-torsorial-constant-walk-Undirected-Graph-𝔽 :
+    is-torsorial constant-walk-Undirected-Graph-𝔽
+  is-torsorial-constant-walk-Undirected-Graph-𝔽 =
+    is-torsorial-constant-walk-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+
+  constant-walk-eq-Undirected-Graph-𝔽 :
+    (y : vertex-Undirected-Graph-𝔽 G) →
+    x ＝ y → constant-walk-Undirected-Graph-𝔽 y
+  constant-walk-eq-Undirected-Graph-𝔽 =
+    constant-walk-eq-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+
+  is-equiv-constant-walk-eq-Undirected-Graph-𝔽 :
+    (y : vertex-Undirected-Graph-𝔽 G) →
+    is-equiv (constant-walk-eq-Undirected-Graph-𝔽 y)
+  is-equiv-constant-walk-eq-Undirected-Graph-𝔽 =
+    is-equiv-constant-walk-eq-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+
+  equiv-constant-walk-eq-Undirected-Graph-𝔽 :
+    (y : vertex-Undirected-Graph-𝔽 G) →
+    (x ＝ y) ≃ constant-walk-Undirected-Graph-𝔽 y
+  equiv-constant-walk-eq-Undirected-Graph-𝔽 =
+    equiv-constant-walk-eq-Undirected-Graph
+      ( undirected-graph-Undirected-Graph-𝔽 G)
+
+  eq-constant-walk-Undirected-Graph-𝔽 :
+    {y : vertex-Undirected-Graph-𝔽 G} →
+    constant-walk-Undirected-Graph-𝔽 y → x ＝ y
+  eq-constant-walk-Undirected-Graph-𝔽 =
+    eq-constant-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
+
+  is-prop-constant-walk-Undirected-Graph-𝔽 :
+    (y : vertex-Undirected-Graph-𝔽 G) →
+    is-prop (constant-walk-Undirected-Graph-𝔽 y)
+  is-prop-constant-walk-Undirected-Graph-𝔽 y =
+    is-prop-equiv'
+      ( equiv-constant-walk-eq-Undirected-Graph-𝔽 y)
+      ( is-set-vertex-Undirected-Graph-𝔽 G x y)
+
+  is-decidable-constant-walk-Undirected-Graph-𝔽 :
+    (y : vertex-Undirected-Graph-𝔽 G) →
+    is-decidable (constant-walk-Undirected-Graph-𝔽 y)
+  is-decidable-constant-walk-Undirected-Graph-𝔽 y =
+    is-decidable-equiv'
+      ( equiv-constant-walk-eq-Undirected-Graph-𝔽 y)
+      ( has-decidable-equality-vertex-Undirected-Graph-𝔽 G x y)
+
+  is-decidable-prop-constant-walk-Undirected-Graph-𝔽 :
+    (y : vertex-Undirected-Graph-𝔽 G) →
+    is-decidable-prop (constant-walk-Undirected-Graph-𝔽 y)
+  pr1 (is-decidable-prop-constant-walk-Undirected-Graph-𝔽 y) =
+    is-prop-constant-walk-Undirected-Graph-𝔽 y
+  pr2 (is-decidable-prop-constant-walk-Undirected-Graph-𝔽 y) =
+    is-decidable-constant-walk-Undirected-Graph-𝔽 y
+```
+
+### The type of walks from `x` to `y` in a finite undirected graph has decidable equality
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  where
+
+  has-decidable-equality-total-walk-of-length-Undirected-Graph-𝔽 :
+    {x y : vertex-Undirected-Graph-𝔽 G} →
+    (n : ℕ) → has-decidable-equality (walk-of-length-Undirected-Graph-𝔽 G n x y)
+  has-decidable-equality-total-walk-of-length-Undirected-Graph-𝔽 .0 refl-walk-of-length-Undirected-Graph w' = inl {!!}
+  has-decidable-equality-total-walk-of-length-Undirected-Graph-𝔽 .(succ-ℕ n) (cons-walk-of-length-Undirected-Graph n p e w) w' = {!!}
+
+  has-decidable-equality-walk-Undirected-Graph-𝔽 :
+    {x y : vertex-Undirected-Graph-𝔽 G} →
+    has-decidable-equality (walk-Undirected-Graph-𝔽 G x y)
+  has-decidable-equality-walk-Undirected-Graph-𝔽 {x} {.x}
+    refl-walk-Undirected-Graph w = {!is-decidable-is-constant-walk-Undirected-Graph-𝔽 G w!}
+  has-decidable-equality-walk-Undirected-Graph-𝔽 {x} {._}
+    ( cons-walk-Undirected-Graph p e v) w =
+    {!!}
+```
diff --git a/src/graph-theory/walks-undirected-graphs.lagda.md b/src/graph-theory/walks-undirected-graphs.lagda.md
index 0377bd1cc9..bf606fdb5f 100644
--- a/src/graph-theory/walks-undirected-graphs.lagda.md
+++ b/src/graph-theory/walks-undirected-graphs.lagda.md
@@ -19,7 +19,9 @@ open import foundation.empty-types
 open import foundation.equivalences
 open import foundation.function-types
 open import foundation.functoriality-coproduct-types
+open import foundation.functoriality-dependent-pair-types
 open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.torsorial-type-families
@@ -39,8 +41,15 @@ open import univalent-combinatorics.standard-finite-types
 
 A **walk** in an [undirected graph](graph-theory.undirected-graphs.md) consists
 of a [list](lists.lists.md) of edges that connect the starting point with the
-end point. Walks may repeat edges and pass through the same vertex multiple
-times.
+end point. More formally, it is defined as the inductive family of types over
+the type of vertices of an undirected graph `G`, with the following constructors
+
+- A **constant walk** `refl : walk-Undirected-Graph G x x` for every vertex `x`.
+- A function `cons e i : walk x (p i) → walk x (p -i)` for every [unordered pair](foundation.unordered-pairs.md) of vertices of `G`, every `e : edge p` and every element `i : type-unordered pair p`.
+
+Note that walks may repeat edges and pass through the same vertex multiple times.
+
+Alternatively, we may define **walks of (fixed) length** `n : ℕ` from `x` to `y` in an undirected graph. The definition of walks of length `n` is similar to the definition of walks, except that we specify the constant walk to have length `0`, and the walk `cons e i w` of a walk `w` of length `n` to have length `n + 1`.
 
 ## Definitions
 
@@ -156,6 +165,121 @@ module _
     succ-ℕ (length-walk-Undirected-Graph w)
 ```
 
+### Walks of a fixed length
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph l1 l2)
+  where
+
+  data walk-of-length-Undirected-Graph :
+    ℕ → (x y : vertex-Undirected-Graph G) → UU (lsuc lzero ⊔ l1 ⊔ l2)
+    where
+    refl-walk-of-length-Undirected-Graph :
+      {x : vertex-Undirected-Graph G} → walk-of-length-Undirected-Graph 0 x x
+    cons-walk-of-length-Undirected-Graph :
+      (n : ℕ) {x : vertex-Undirected-Graph G}
+      (p : unordered-pair-vertices-Undirected-Graph G)
+      (e : edge-Undirected-Graph G p) {i : type-unordered-pair p} →
+      walk-of-length-Undirected-Graph n x (element-unordered-pair p i) →
+      walk-of-length-Undirected-Graph
+        ( succ-ℕ n)
+        ( x)
+        ( other-element-unordered-pair p i)
+
+  map-compute-total-walk-of-length-Undirected-Graph :
+    (x y : vertex-Undirected-Graph G) →
+    walk-Undirected-Graph G x y →
+    Σ ℕ (λ n → walk-of-length-Undirected-Graph n x y)
+  map-compute-total-walk-of-length-Undirected-Graph x .x
+    refl-walk-Undirected-Graph =
+    ( 0 , refl-walk-of-length-Undirected-Graph)
+  map-compute-total-walk-of-length-Undirected-Graph x ._
+    ( cons-walk-Undirected-Graph p e w) =
+    map-Σ
+      ( λ n →
+        walk-of-length-Undirected-Graph n x (other-element-unordered-pair p _))
+      ( succ-ℕ)
+      ( λ n → cons-walk-of-length-Undirected-Graph n p e)
+      ( map-compute-total-walk-of-length-Undirected-Graph
+        ( x)
+        ( element-unordered-pair p _)
+        ( w))
+
+  map-inv-compute-total-walk-of-length-Undirected-Graph :
+    (x y : vertex-Undirected-Graph G) →
+    Σ ℕ (λ n → walk-of-length-Undirected-Graph n x y) →
+    walk-Undirected-Graph G x y
+  map-inv-compute-total-walk-of-length-Undirected-Graph x y
+    ( .0 , refl-walk-of-length-Undirected-Graph) =
+    refl-walk-Undirected-Graph
+  map-inv-compute-total-walk-of-length-Undirected-Graph x
+    .(other-element-unordered-pair p _)
+    (.(succ-ℕ n) , cons-walk-of-length-Undirected-Graph n p e w) =
+    cons-walk-Undirected-Graph p e
+      ( map-inv-compute-total-walk-of-length-Undirected-Graph
+        ( x)
+        ( element-unordered-pair p _)
+        ( n , w))
+
+  is-section-map-inv-compute-total-walk-of-length-Undirected-Graph :
+    (x y : vertex-Undirected-Graph G) →
+    ( map-compute-total-walk-of-length-Undirected-Graph x y ∘
+      map-inv-compute-total-walk-of-length-Undirected-Graph x y) ~ id
+  is-section-map-inv-compute-total-walk-of-length-Undirected-Graph x y
+    ( .0 , refl-walk-of-length-Undirected-Graph) =
+    refl
+  is-section-map-inv-compute-total-walk-of-length-Undirected-Graph x
+    .(other-element-unordered-pair p _)
+    (.(succ-ℕ n) , cons-walk-of-length-Undirected-Graph n p e w) =
+    ap
+      ( map-Σ
+        ( λ n →
+          walk-of-length-Undirected-Graph n x
+            ( other-element-unordered-pair p _))
+        ( succ-ℕ)
+        ( λ n → cons-walk-of-length-Undirected-Graph n p e))
+      ( is-section-map-inv-compute-total-walk-of-length-Undirected-Graph
+        ( x)
+        ( element-unordered-pair p _)
+        ( n , w))
+
+  is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph :
+    (x y : vertex-Undirected-Graph G) →
+    ( map-inv-compute-total-walk-of-length-Undirected-Graph x y ∘
+      map-compute-total-walk-of-length-Undirected-Graph x y) ~ id
+  is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph x y
+    refl-walk-Undirected-Graph =
+    refl
+  is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph x
+    .(other-element-unordered-pair p _)
+    (cons-walk-Undirected-Graph p e w) =
+    ap
+      ( cons-walk-Undirected-Graph p e)
+      ( is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph
+        ( x)
+        ( element-unordered-pair p _)
+        ( w))
+
+  is-equiv-map-compute-total-walk-of-length-Undirected-Graph :
+    (x y : vertex-Undirected-Graph G) →
+    is-equiv (map-compute-total-walk-of-length-Undirected-Graph x y)
+  is-equiv-map-compute-total-walk-of-length-Undirected-Graph x y =
+    is-equiv-is-invertible
+      ( map-inv-compute-total-walk-of-length-Undirected-Graph x y)
+      ( is-section-map-inv-compute-total-walk-of-length-Undirected-Graph x y)
+      ( is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph x y)
+
+  compute-total-walk-of-length-Undirected-Graph :
+    (x y : vertex-Undirected-Graph G) →
+    walk-Undirected-Graph G x y ≃
+    Σ ℕ (λ n → walk-of-length-Undirected-Graph n x y)
+  pr1 (compute-total-walk-of-length-Undirected-Graph x y) =
+    map-compute-total-walk-of-length-Undirected-Graph x y
+  pr2 (compute-total-walk-of-length-Undirected-Graph x y) =
+    is-equiv-map-compute-total-walk-of-length-Undirected-Graph x y
+```
+
 ## Properties
 
 ### The type of vertices on the constant walk is contractible
@@ -165,10 +289,10 @@ module _
   {l1 l2 : Level} (G : Undirected-Graph l1 l2) (x : vertex-Undirected-Graph G)
   where
 
-  is-contr-vertex-on-walk-refl-walk-Undirected-Graph :
+  is-contr-vertex-on-refl-walk-Undirected-Graph :
     is-contr
       ( vertex-on-walk-Undirected-Graph G (refl-walk-Undirected-Graph {x = x}))
-  is-contr-vertex-on-walk-refl-walk-Undirected-Graph =
+  is-contr-vertex-on-refl-walk-Undirected-Graph =
     is-torsorial-path x
 ```
 
@@ -185,7 +309,7 @@ module _
     Fin (succ-ℕ (length-walk-Undirected-Graph G w))
   compute-vertex-on-walk-Undirected-Graph refl-walk-Undirected-Graph =
     equiv-is-contr
-      ( is-contr-vertex-on-walk-refl-walk-Undirected-Graph G x)
+      ( is-contr-vertex-on-refl-walk-Undirected-Graph G x)
       ( is-contr-Fin-one-ℕ)
   compute-vertex-on-walk-Undirected-Graph
     ( cons-walk-Undirected-Graph p e {y} w) =
@@ -450,16 +574,16 @@ module _
   {l1 l2 : Level} (G : Undirected-Graph l1 l2) {x : vertex-Undirected-Graph G}
   where
 
-  is-constant-walk-Undirected-Graph-Prop :
+  is-constant-prop-walk-Undirected-Graph :
     {y : vertex-Undirected-Graph G} →
     walk-Undirected-Graph G x y → Prop lzero
-  is-constant-walk-Undirected-Graph-Prop w =
+  is-constant-prop-walk-Undirected-Graph w =
     is-zero-ℕ-Prop (length-walk-Undirected-Graph G w)
 
   is-constant-walk-Undirected-Graph :
     {y : vertex-Undirected-Graph G} → walk-Undirected-Graph G x y → UU lzero
   is-constant-walk-Undirected-Graph w =
-    type-Prop (is-constant-walk-Undirected-Graph-Prop w)
+    type-Prop (is-constant-prop-walk-Undirected-Graph w)
 
   constant-walk-Undirected-Graph :
     (y : vertex-Undirected-Graph G) → UU (lsuc lzero ⊔ l1 ⊔ l2)
diff --git a/src/organic-chemistry/ethane.lagda.md b/src/organic-chemistry/ethane.lagda.md
index d7481fc5be..e98b451752 100644
--- a/src/organic-chemistry/ethane.lagda.md
+++ b/src/organic-chemistry/ethane.lagda.md
@@ -30,7 +30,7 @@ open import foundation.univalence
 open import foundation.universe-levels
 open import foundation.unordered-pairs
 
-open import graph-theory.finite-graphs
+open import graph-theory.finite-undirected-graphs
 open import graph-theory.walks-undirected-graphs
 
 open import organic-chemistry.alkanes
diff --git a/src/organic-chemistry/hydrocarbons.lagda.md b/src/organic-chemistry/hydrocarbons.lagda.md
index ec8fbcf5a5..40f0115304 100644
--- a/src/organic-chemistry/hydrocarbons.lagda.md
+++ b/src/organic-chemistry/hydrocarbons.lagda.md
@@ -19,7 +19,7 @@ open import foundation.universe-levels
 open import foundation.unordered-pairs
 
 open import graph-theory.connected-undirected-graphs
-open import graph-theory.finite-graphs
+open import graph-theory.finite-undirected-graphs
 
 open import univalent-combinatorics.finite-types
 ```
diff --git a/src/trees/directed-trees.lagda.md b/src/trees/directed-trees.lagda.md
index f51317af6f..486c63d03f 100644
--- a/src/trees/directed-trees.lagda.md
+++ b/src/trees/directed-trees.lagda.md
@@ -47,10 +47,10 @@ that for every vertex `x : G` the type of walks from `x` to `r` is contractible.
 ## Definition
 
 ```agda
-is-tree-Directed-Graph-Prop' :
+is-tree-prop-Directed-Graph' :
   {l1 l2 : Level} (G : Directed-Graph l1 l2) (r : vertex-Directed-Graph G) →
   Prop (l1 ⊔ l2)
-is-tree-Directed-Graph-Prop' G r =
+is-tree-prop-Directed-Graph' G r =
   Π-Prop
     ( vertex-Directed-Graph G)
     ( λ x → is-contr-Prop (walk-Directed-Graph G x r))
@@ -58,13 +58,13 @@ is-tree-Directed-Graph-Prop' G r =
 is-tree-Directed-Graph' :
   {l1 l2 : Level} (G : Directed-Graph l1 l2) (r : vertex-Directed-Graph G) →
   UU (l1 ⊔ l2)
-is-tree-Directed-Graph' G r = type-Prop (is-tree-Directed-Graph-Prop' G r)
+is-tree-Directed-Graph' G r = type-Prop (is-tree-prop-Directed-Graph' G r)
 
 is-prop-is-tree-Directed-Graph' :
   {l1 l2 : Level} (G : Directed-Graph l1 l2) (r : vertex-Directed-Graph G) →
   is-prop (is-tree-Directed-Graph' G r)
 is-prop-is-tree-Directed-Graph' G r =
-  is-prop-type-Prop (is-tree-Directed-Graph-Prop' G r)
+  is-prop-type-Prop (is-tree-prop-Directed-Graph' G r)
 
 is-tree-Directed-Graph :
   {l1 l2 : Level} → Directed-Graph l1 l2 → UU (l1 ⊔ l2)
@@ -231,12 +231,12 @@ module _
     is-prop-all-elements-equal
       ( λ H K →
         eq-type-subtype
-          ( is-tree-Directed-Graph-Prop' G)
+          ( is-tree-prop-Directed-Graph' G)
           ( uniqueness-root-is-tree-Directed-Graph H K))
 
-  is-tree-directed-graph-Prop : Prop (l1 ⊔ l2)
-  pr1 is-tree-directed-graph-Prop = is-tree-Directed-Graph G
-  pr2 is-tree-directed-graph-Prop = is-prop-is-tree-Directed-Graph
+  is-tree-prop-Directed-Graph : Prop (l1 ⊔ l2)
+  pr1 is-tree-prop-Directed-Graph = is-tree-Directed-Graph G
+  pr2 is-tree-prop-Directed-Graph = is-prop-is-tree-Directed-Graph
 
 uniqueness-root-Directed-Tree :
   {l1 l2 : Level} (T : Directed-Tree l1 l2)
diff --git a/src/trees/equivalences-directed-trees.lagda.md b/src/trees/equivalences-directed-trees.lagda.md
index 3d53b85582..de245231b3 100644
--- a/src/trees/equivalences-directed-trees.lagda.md
+++ b/src/trees/equivalences-directed-trees.lagda.md
@@ -424,7 +424,7 @@ module _
     (S : Directed-Tree l1 l2) → (T ＝ S) ≃ equiv-Directed-Tree T S
   extensionality-Directed-Tree =
     extensionality-type-subtype
-      ( is-tree-directed-graph-Prop)
+      ( is-tree-prop-Directed-Graph)
       ( is-tree-Directed-Tree T)
       ( id-equiv-Directed-Graph (graph-Directed-Tree T))
       ( extensionality-Directed-Graph (graph-Directed-Tree T))
diff --git a/src/trees/undirected-trees.lagda.md b/src/trees/undirected-trees.lagda.md
index b9317cfec2..3c0c476f2c 100644
--- a/src/trees/undirected-trees.lagda.md
+++ b/src/trees/undirected-trees.lagda.md
@@ -211,7 +211,7 @@ module _
   is-constant-walk-Undirected-Tree-Prop :
     {x y : node-Undirected-Tree} → walk-Undirected-Tree x y → Prop lzero
   is-constant-walk-Undirected-Tree-Prop =
-    is-constant-walk-Undirected-Graph-Prop undirected-graph-Undirected-Tree
+    is-constant-prop-walk-Undirected-Graph undirected-graph-Undirected-Tree
 
   is-constant-walk-Undirected-Tree :
     {x y : node-Undirected-Tree} → walk-Undirected-Tree x y → UU lzero
@@ -228,7 +228,7 @@ module _
   is-constant-trail-Undirected-Tree-Prop :
     {x y : node-Undirected-Tree} → trail-Undirected-Tree x y → Prop lzero
   is-constant-trail-Undirected-Tree-Prop =
-    is-constant-trail-Undirected-Graph-Prop undirected-graph-Undirected-Tree
+    is-constant-prop-trail-Undirected-Graph undirected-graph-Undirected-Tree
 
   is-constant-trail-Undirected-Tree :
     {x y : node-Undirected-Tree} → trail-Undirected-Tree x y → UU lzero