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/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/finite-graphs.lagda.md → src/graph-theory/finite-undirected-graphs.lagda.md

@@ -1,22 +1,29 @@
 # Finite 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-Undirected-Graph-Prop : Prop (lsuc lzero ⊔ l1 ⊔ l2)
+  is-finite-Undirected-Graph-Prop =
+    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-Undirected-Graph-Prop
+
+  is-prop-is-finite-Undirected-Graph :
+    is-prop is-finite-Undirected-Graph
+  is-prop-is-finite-Undirected-Graph =
+    is-prop-type-Prop is-finite-Undirected-Graph-Prop
+```
+
 ### 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
+```

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

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 _