From 810b63c688943964b797b3e356c934fc534dc8bc Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 22 Oct 2023 20:00:20 +0200
Subject: [PATCH] update graph theory

---
 src/graph-theory.lagda.md                                | 6 +++++-
 src/graph-theory/walks-finite-undirected-graphs.lagda.md | 9 +++++----
 src/organic-chemistry/ethane.lagda.md                    | 2 +-
 src/organic-chemistry/hydrocarbons.lagda.md              | 2 +-
 4 files changed, 12 insertions(+), 7 deletions(-)

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/walks-finite-undirected-graphs.lagda.md b/src/graph-theory/walks-finite-undirected-graphs.lagda.md
index fddf843f10..bcfac81e45 100644
--- a/src/graph-theory/walks-finite-undirected-graphs.lagda.md
+++ b/src/graph-theory/walks-finite-undirected-graphs.lagda.md
@@ -24,6 +24,7 @@ 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
 
@@ -470,10 +471,10 @@ module _
   refl-constant-walk-Undirected-Graph-𝔽 =
     refl-constant-walk-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G)
 
-  is-contr-total-constant-walk-Undirected-Graph-𝔽 :
-    is-contr (Σ (vertex-Undirected-Graph-𝔽 G) constant-walk-Undirected-Graph-𝔽)
-  is-contr-total-constant-walk-Undirected-Graph-𝔽 =
-    is-contr-total-constant-walk-Undirected-Graph
+  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-𝔽 :
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
 ```