Refactor graphs with updates from Beyond finite sets

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

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)

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
 ```
 

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
 ```

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

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

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
 ```

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

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 =

src/graph-theory/faithful-morphisms-undirected-graphs.lagda.md

@@ -42,23 +42,23 @@ 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))
 
   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 =

src/graph-theory/finite-graphs.lagda.md → 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,13 +105,38 @@ 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-𝔽
 
   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-𝔽

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
+```