update graph theory

UniMath · Oct 22, 2023 · 810b63c · 810b63c
1 parent 828dd0c
commit 810b63c
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
 ```