diff --git a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md index b9f0763a29..0a66689361 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/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/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..d7e3fe7cc2 100644 --- a/src/graph-theory/finite-graphs.lagda.md +++ b/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 ```
Imports ```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,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 +``` + +
Imports + +```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 +``` + +
+ +## 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 +``` + +
Imports + +```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 +``` + +
+ +## 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/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/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 +``` + +
Imports + +```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 +``` + +
+ +## 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..1fa6d13545 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..fddf843f10 --- /dev/null +++ b/src/graph-theory/walks-finite-undirected-graphs.lagda.md @@ -0,0 +1,546 @@ +# Walks in finite undirected graphs + +```agda +{-# OPTIONS --allow-unsolved-metas #-} + +module graph-theory.walks-finite-undirected-graphs where +``` + +
Imports + +```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.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 +``` + +
+ +## 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) + (x : vertex-Undirected-Graph-𝔽 G) + where + + walk-of-length-Undirected-Graph-𝔽 : + ℕ → vertex-Undirected-Graph-𝔽 G → UU (lsuc lzero ⊔ l1 ⊔ l2) + walk-of-length-Undirected-Graph-𝔽 = + walk-of-length-Undirected-Graph (undirected-graph-Undirected-Graph-𝔽 G) x + + map-compute-total-walk-of-length-Undirected-Graph-𝔽 : + (y : vertex-Undirected-Graph-𝔽 G) → + walk-Undirected-Graph-𝔽 G x y → + Σ ℕ (λ n → walk-of-length-Undirected-Graph-𝔽 n y) + map-compute-total-walk-of-length-Undirected-Graph-𝔽 = + map-compute-total-walk-of-length-Undirected-Graph + ( undirected-graph-Undirected-Graph-𝔽 G) + ( x) + + map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 : + (y : vertex-Undirected-Graph-𝔽 G) → + Σ ℕ (λ n → walk-of-length-Undirected-Graph-𝔽 n 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) + ( x) + + is-section-map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 : + (y : vertex-Undirected-Graph-𝔽 G) → + ( map-compute-total-walk-of-length-Undirected-Graph-𝔽 y ∘ + map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 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) + ( x) + + is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 : + (y : vertex-Undirected-Graph-𝔽 G) → + ( map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 y ∘ + map-compute-total-walk-of-length-Undirected-Graph-𝔽 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) + ( x) + + is-equiv-map-compute-total-walk-of-length-Undirected-Graph-𝔽 : + (y : vertex-Undirected-Graph-𝔽 G) → + is-equiv (map-compute-total-walk-of-length-Undirected-Graph-𝔽 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) + ( x) + + compute-total-walk-of-length-Undirected-Graph-𝔽 : + (y : vertex-Undirected-Graph-𝔽 G) → + walk-Undirected-Graph-𝔽 G x y ≃ + Σ ℕ (λ n → walk-of-length-Undirected-Graph-𝔽 n y) + compute-total-walk-of-length-Undirected-Graph-𝔽 = + compute-total-walk-of-length-Undirected-Graph + ( undirected-graph-Undirected-Graph-𝔽 G) + ( x) +``` + +## 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-walk-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-walk-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-walk-Undirected-Graph-Prop + ( 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-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 + ( 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-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 = + {!!} + 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..6b6d563ddd 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 @@ -156,6 +158,114 @@ module _ succ-ℕ (length-walk-Undirected-Graph w) ``` +### Walks of a fixed length + +```agda +module _ + {l1 l2 : Level} (G : Undirected-Graph l1 l2) (x : vertex-Undirected-Graph G) + where + + data walk-of-length-Undirected-Graph : + ℕ → vertex-Undirected-Graph G → UU (lsuc lzero ⊔ l1 ⊔ l2) + where + refl-walk-of-length-Undirected-Graph : + walk-of-length-Undirected-Graph 0 x + cons-walk-of-length-Undirected-Graph : + (n : ℕ) (p : unordered-pair-vertices-Undirected-Graph G) + (e : edge-Undirected-Graph G p) {i : type-unordered-pair p} → + walk-of-length-Undirected-Graph n (element-unordered-pair p i) → + walk-of-length-Undirected-Graph + ( succ-ℕ n) + ( other-element-unordered-pair p i) + + map-compute-total-walk-of-length-Undirected-Graph : + (y : vertex-Undirected-Graph G) → + walk-Undirected-Graph G x y → + Σ ℕ (λ n → walk-of-length-Undirected-Graph n y) + map-compute-total-walk-of-length-Undirected-Graph .x + refl-walk-Undirected-Graph = + ( 0 , refl-walk-of-length-Undirected-Graph) + map-compute-total-walk-of-length-Undirected-Graph ._ + ( cons-walk-Undirected-Graph p e w) = + map-Σ + ( λ n → + walk-of-length-Undirected-Graph n (other-element-unordered-pair p _)) + ( succ-ℕ) + ( λ n → cons-walk-of-length-Undirected-Graph n p e) + ( map-compute-total-walk-of-length-Undirected-Graph + ( element-unordered-pair p _) + ( w)) + + map-inv-compute-total-walk-of-length-Undirected-Graph : + (y : vertex-Undirected-Graph G) → + Σ ℕ (λ n → walk-of-length-Undirected-Graph n y) → + walk-Undirected-Graph G x y + map-inv-compute-total-walk-of-length-Undirected-Graph y + ( .0 , refl-walk-of-length-Undirected-Graph) = + refl-walk-Undirected-Graph + map-inv-compute-total-walk-of-length-Undirected-Graph + .(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 + ( element-unordered-pair p _) + ( n , w)) + + is-section-map-inv-compute-total-walk-of-length-Undirected-Graph : + (y : vertex-Undirected-Graph G) → + ( map-compute-total-walk-of-length-Undirected-Graph y ∘ + map-inv-compute-total-walk-of-length-Undirected-Graph y) ~ id + is-section-map-inv-compute-total-walk-of-length-Undirected-Graph y + ( .0 , refl-walk-of-length-Undirected-Graph) = + refl + is-section-map-inv-compute-total-walk-of-length-Undirected-Graph + .(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 (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 + ( element-unordered-pair p _) + ( n , w)) + + is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph : + (y : vertex-Undirected-Graph G) → + ( map-inv-compute-total-walk-of-length-Undirected-Graph y ∘ + map-compute-total-walk-of-length-Undirected-Graph y) ~ id + is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph y + refl-walk-Undirected-Graph = + refl + is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph + .(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 + ( element-unordered-pair p _) + ( w)) + + is-equiv-map-compute-total-walk-of-length-Undirected-Graph : + (y : vertex-Undirected-Graph G) → + is-equiv (map-compute-total-walk-of-length-Undirected-Graph y) + is-equiv-map-compute-total-walk-of-length-Undirected-Graph y = + is-equiv-is-invertible + ( map-inv-compute-total-walk-of-length-Undirected-Graph y) + ( is-section-map-inv-compute-total-walk-of-length-Undirected-Graph y) + ( is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph y) + + compute-total-walk-of-length-Undirected-Graph : + (y : vertex-Undirected-Graph G) → + walk-Undirected-Graph G x y ≃ + Σ ℕ (λ n → walk-of-length-Undirected-Graph n y) + pr1 (compute-total-walk-of-length-Undirected-Graph y) = + map-compute-total-walk-of-length-Undirected-Graph y + pr2 (compute-total-walk-of-length-Undirected-Graph y) = + is-equiv-map-compute-total-walk-of-length-Undirected-Graph y +``` + ## Properties ### The type of vertices on the constant walk is contractible 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.lagda.md b/src/trees.lagda.md index a2f7fd445b..c6f70eb2e2 100644 --- a/src/trees.lagda.md +++ b/src/trees.lagda.md @@ -28,6 +28,7 @@ open import trees.equivalences-enriched-directed-trees public open import trees.extensional-w-types public open import trees.fibers-directed-trees public open import trees.fibers-enriched-directed-trees public +open import trees.finite-undirected-trees public open import trees.functoriality-combinator-directed-trees public open import trees.functoriality-fiber-directed-tree public open import trees.functoriality-w-types public diff --git a/src/trees/finite-undirected-trees.lagda.md b/src/trees/finite-undirected-trees.lagda.md new file mode 100644 index 0000000000..4341cdb996 --- /dev/null +++ b/src/trees/finite-undirected-trees.lagda.md @@ -0,0 +1,169 @@ +# Finite undirected trees + +```agda +{-# OPTIONS --allow-unsolved-metas #-} + +module trees.finite-undirected-trees where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.decidable-propositions +open import foundation.decidable-types +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.propositions +open import foundation.universe-levels +open import foundation.unordered-pairs + +open import graph-theory.finite-undirected-graphs + +open import trees.undirected-trees + +open import univalent-combinatorics.decidable-dependent-function-types +open import univalent-combinatorics.decidable-propositions +open import univalent-combinatorics.finite-types +open import univalent-combinatorics.pi-finite-types +open import univalent-combinatorics.symmetric-operations +``` + +
+ +## Idea + +A **finite undirected tree** is a finite undirected graph such that between any +two nodes there is a unique trail. + +## Definitions + +### The predicate of being a finite undirected tree + +```agda +module _ + {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2) + where + + is-tree-Undirected-Graph-𝔽-Prop : Prop (lsuc lzero ⊔ l1 ⊔ l2) + is-tree-Undirected-Graph-𝔽-Prop = + is-tree-Undirected-Graph-Prop + ( undirected-graph-Undirected-Graph-𝔽 G) + + is-tree-Undirected-Graph-𝔽 : UU (lsuc lzero ⊔ l1 ⊔ l2) + is-tree-Undirected-Graph-𝔽 = + type-Prop is-tree-Undirected-Graph-𝔽-Prop +``` + +### The type of finite undirected trees + +```agda +Undirected-Tree-𝔽 : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +Undirected-Tree-𝔽 l1 l2 = + Σ (Undirected-Graph-𝔽 l1 l2) is-tree-Undirected-Graph-𝔽 +``` + +### Finite trees of cardinality `n` + +```agda +Undirected-Tree-Of-Size : + (l1 l2 : Level) (n : ℕ) → UU (lsuc l1) +Undirected-Tree-Of-Size l1 l2 n = + Σ ( UU-Fin l1 n) + ( λ V → + Σ ( unordered-pair (type-UU-Fin n V) → Decidable-Prop lzero) + ( λ E → + is-tree-Undirected-Graph + ( type-UU-Fin n V , λ p → type-Decidable-Prop (E p)))) + +module _ + {l1 l2 : Level} (n : ℕ) (T : Undirected-Tree-Of-Size l1 l2 n) + where + + node-Undirected-Tree-Of-Size : UU l1 + node-Undirected-Tree-Of-Size = type-UU-Fin n (pr1 T) + + has-cardinality-node-Undirected-Tree-Of-Size : + has-cardinality n node-Undirected-Tree-Of-Size + has-cardinality-node-Undirected-Tree-Of-Size = + has-cardinality-type-UU-Fin n (pr1 T) + + is-finite-node-Undirected-Tree-Of-Size : + is-finite node-Undirected-Tree-Of-Size + is-finite-node-Undirected-Tree-Of-Size = + is-finite-has-cardinality n has-cardinality-node-Undirected-Tree-Of-Size + + node-finite-type-Undirected-Tree-Of-Size : 𝔽 l1 + pr1 node-finite-type-Undirected-Tree-Of-Size = + node-Undirected-Tree-Of-Size + pr2 node-finite-type-Undirected-Tree-Of-Size = + is-finite-node-Undirected-Tree-Of-Size + + unordered-pair-nodes-Undirected-Tree-Of-Size : UU (lsuc lzero ⊔ l1) + unordered-pair-nodes-Undirected-Tree-Of-Size = + unordered-pair node-Undirected-Tree-Of-Size + + edge-decidable-prop-Undirected-Tree-Of-Size : + unordered-pair-nodes-Undirected-Tree-Of-Size → Decidable-Prop lzero + edge-decidable-prop-Undirected-Tree-Of-Size = pr1 (pr2 T) + + edge-Undirected-Tree-Of-Size : + unordered-pair-nodes-Undirected-Tree-Of-Size → UU lzero + edge-Undirected-Tree-Of-Size = + type-Decidable-Prop ∘ edge-decidable-prop-Undirected-Tree-Of-Size + + is-decidable-prop-edge-Undirected-Tree-Of-Size : + (p : unordered-pair-nodes-Undirected-Tree-Of-Size) → + is-decidable-prop (edge-Undirected-Tree-Of-Size p) + is-decidable-prop-edge-Undirected-Tree-Of-Size p = + is-decidable-prop-type-Decidable-Prop + ( edge-decidable-prop-Undirected-Tree-Of-Size p) + + is-finite-edge-Undirected-Tree-Of-Size : + (p : unordered-pair-nodes-Undirected-Tree-Of-Size) → + is-finite (edge-Undirected-Tree-Of-Size p) + is-finite-edge-Undirected-Tree-Of-Size p = + is-finite-type-Decidable-Prop + ( edge-decidable-prop-Undirected-Tree-Of-Size p) +``` + +## Properties + +### The predicate of being a tree on finite undirected graphs is decidable + +```agda +module _ + {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2) + where + + is-decidable-is-tree-Undirected-Graph-𝔽 : + is-decidable (is-tree-Undirected-Graph-𝔽 G) + is-decidable-is-tree-Undirected-Graph-𝔽 = + is-decidable-Π-is-finite + ( is-finite-vertex-Undirected-Graph-𝔽 G) + ( λ x → + is-decidable-Π-is-finite + ( is-finite-vertex-Undirected-Graph-𝔽 G) + ( λ y → + {!!})) +``` + +### The type of finite undirected trees of cardinality `n` is π-finite + +```agda +is-π-finite-Undirected-Tree-Of-Size : + (k n : ℕ) → is-π-finite k (Undirected-Tree-Of-Size lzero lzero n) +is-π-finite-Undirected-Tree-Of-Size k n = + is-π-finite-Σ k + ( is-π-finite-UU-Fin (succ-ℕ k) n) + ( λ (X , H) → + is-π-finite-Σ k + ( is-π-finite-is-finite + ( succ-ℕ k) + ( is-finite-symmetric-operation + ( is-finite-has-cardinality n H) + ( is-finite-Decidable-Prop))) + ( λ E → + is-π-finite-is-finite k {!!})) +``` diff --git a/src/trees/undirected-trees.lagda.md b/src/trees/undirected-trees.lagda.md index b9317cfec2..8de1cef567 100644 --- a/src/trees/undirected-trees.lagda.md +++ b/src/trees/undirected-trees.lagda.md @@ -39,6 +39,17 @@ x to y is contractible for any two vertices x and y. ## Definition ```agda +is-tree-Undirected-Graph-Prop : + {l1 l2 : Level} (G : Undirected-Graph l1 l2) → Prop (lsuc lzero ⊔ l1 ⊔ l2) +is-tree-Undirected-Graph-Prop G = + Π-Prop + ( vertex-Undirected-Graph G) + ( λ x → + Π-Prop + ( vertex-Undirected-Graph G) + ( λ y → + is-contr-Prop (trail-Undirected-Graph G x y))) + is-tree-Undirected-Graph : {l1 l2 : Level} (G : Undirected-Graph l1 l2) → UU (lsuc lzero ⊔ l1 ⊔ l2) is-tree-Undirected-Graph G = diff --git a/src/univalent-combinatorics.lagda.md b/src/univalent-combinatorics.lagda.md index 0cbecf9212..4ca10397fd 100644 --- a/src/univalent-combinatorics.lagda.md +++ b/src/univalent-combinatorics.lagda.md @@ -26,6 +26,7 @@ open import univalent-combinatorics.2-element-types public open import univalent-combinatorics.binomial-types public open import univalent-combinatorics.bracelets public open import univalent-combinatorics.cartesian-product-types public +open import univalent-combinatorics.category-of-cyclically-ordered-types public open import univalent-combinatorics.classical-finite-types public open import univalent-combinatorics.complements-isolated-elements public open import univalent-combinatorics.coproduct-types public @@ -75,7 +76,9 @@ open import univalent-combinatorics.latin-squares public open import univalent-combinatorics.main-classes-of-latin-hypercubes public open import univalent-combinatorics.main-classes-of-latin-squares public open import univalent-combinatorics.maybe public +open import univalent-combinatorics.morphisms-cyclic-types public open import univalent-combinatorics.necklaces public +open import univalent-combinatorics.omega-finite-types public open import univalent-combinatorics.orientations-complete-undirected-graph public open import univalent-combinatorics.orientations-cubes public open import univalent-combinatorics.partitions public @@ -85,6 +88,7 @@ open import univalent-combinatorics.pigeonhole-principle public open import univalent-combinatorics.presented-pi-finite-types public open import univalent-combinatorics.quotients-finite-types public open import univalent-combinatorics.ramsey-theory public +open import univalent-combinatorics.reduced-1-bordism-category public open import univalent-combinatorics.repetitions-of-values public open import univalent-combinatorics.repetitions-of-values-sequences public open import univalent-combinatorics.retracts-of-finite-types public @@ -101,6 +105,7 @@ open import univalent-combinatorics.steiner-triple-systems public open import univalent-combinatorics.sums-of-natural-numbers public open import univalent-combinatorics.surjective-maps public open import univalent-combinatorics.symmetric-difference public +open import univalent-combinatorics.symmetric-operations public open import univalent-combinatorics.trivial-sigma-decompositions public open import univalent-combinatorics.type-duality public open import univalent-combinatorics.unions-subtypes public @@ -108,4 +113,5 @@ open import univalent-combinatorics.universal-property-standard-finite-types pub open import univalent-combinatorics.unlabeled-partitions public open import univalent-combinatorics.unlabeled-rooted-trees public open import univalent-combinatorics.unlabeled-trees public +open import univalent-combinatorics.unordered-pairs-of-elements-finite-types public ``` diff --git a/src/univalent-combinatorics/category-of-cyclically-ordered-types.lagda.md b/src/univalent-combinatorics/category-of-cyclically-ordered-types.lagda.md new file mode 100644 index 0000000000..0f01c9bc95 --- /dev/null +++ b/src/univalent-combinatorics/category-of-cyclically-ordered-types.lagda.md @@ -0,0 +1,27 @@ +# The category of cyclically ordered types + +```agda +module univalent-combinatorics.category-of-cyclically-ordered-types where +``` + +
Imports + +```agda + +``` + +
+ +## Idea + +The **category `Λ` of cyclically ordered types** consists of: + +- Objects are cyclically ordered sets of finite order. +- Morphisms are maps `C m → C n` such that for each point `x : C m` the induced + map `L m → L n` on linear orders is order preserving. + +The geometric realization of the categoy `Λ` should be `ℂP∞`. + +It can also be described as the category of pairs `(M,U)` where `M` is a circle +and `U` is a disjoint union of intervals in `M`. The morphisms from `(M,U)` to +`(N,V)` are the oriented diffeomorphisms `φ : M → N` such that `φ U ⊆ V`. diff --git a/src/univalent-combinatorics/cyclic-finite-types.lagda.md b/src/univalent-combinatorics/cyclic-finite-types.lagda.md index 649904a36d..3e2b0a7515 100644 --- a/src/univalent-combinatorics/cyclic-finite-types.lagda.md +++ b/src/univalent-combinatorics/cyclic-finite-types.lagda.md @@ -1,6 +1,8 @@ # Cyclic finite types ```agda +{-# OPTIONS --allow-unsolved-metas #-} + module univalent-combinatorics.cyclic-finite-types where ``` @@ -8,6 +10,7 @@ module univalent-combinatorics.cyclic-finite-types where ```agda open import elementary-number-theory.addition-integers +open import elementary-number-theory.inequality-standard-finite-types open import elementary-number-theory.integers open import elementary-number-theory.modular-arithmetic open import elementary-number-theory.modular-arithmetic-standard-finite-types @@ -53,9 +56,11 @@ open import synthetic-homotopy-theory.loop-spaces ## Idea -A cyclic type is a type `X` equipped with an endomorphism `f : X → X` such that -the pair `(X, f)` is merely equivalent to the pair `(ℤ-Mod k, +1)` for some -`k : ℕ`. +A cyclic type is a +[type `X` equipped with an endomorphism](structured-types.types-equipped-with-endomorphisms.md) +`f : X → X` such that the pair `(X, f)` is +[merely equivalent](structured-types.mere-equivalences-types-equipped-with-endomorphisms.md) +to the pair `(ℤ-Mod k, +1)` for some `k : ℕ`. ## Definitions @@ -221,6 +226,8 @@ module _ ## Properties +### Characterization of equality of equivalences of cyclic types + ```agda module _ {l1 l2 : Level} (k : ℕ) (X : Cyclic-Type l1 k) (Y : Cyclic-Type l2 k) @@ -286,7 +293,11 @@ module _ (e f : equiv-Cyclic-Type k X Y) → htpy-equiv-Cyclic-Type e f → e ＝ f eq-htpy-equiv-Cyclic-Type e f = map-inv-equiv (extensionality-equiv-Cyclic-Type e f) +``` +### Composition of equivalences of cyclic types + +```agda comp-equiv-Cyclic-Type : {l1 l2 l3 : Level} (k : ℕ) (X : Cyclic-Type l1 k) (Y : Cyclic-Type l2 k) (Z : Cyclic-Type l3 k) → @@ -296,7 +307,11 @@ comp-equiv-Cyclic-Type k X Y Z = ( endo-Cyclic-Type k X) ( endo-Cyclic-Type k Y) ( endo-Cyclic-Type k Z) +``` +### Inverses of equivalences of cyclic types + +```agda inv-equiv-Cyclic-Type : {l1 l2 : Level} (k : ℕ) (X : Cyclic-Type l1 k) (Y : Cyclic-Type l2 k) → equiv-Cyclic-Type k X Y → equiv-Cyclic-Type k Y X @@ -304,7 +319,11 @@ inv-equiv-Cyclic-Type k X Y = inv-equiv-Type-With-Endomorphism ( endo-Cyclic-Type k X) ( endo-Cyclic-Type k Y) +``` +### Associativity of composition of equivalences of cyclic types + +```agda associative-comp-equiv-Cyclic-Type : {l1 l2 l3 l4 : Level} (k : ℕ) (X : Cyclic-Type l1 k) (Y : Cyclic-Type l2 k) (Z : Cyclic-Type l3 k) (W : Cyclic-Type l4 k) (g : equiv-Cyclic-Type k Z W) @@ -320,7 +339,11 @@ associative-comp-equiv-Cyclic-Type k X Y Z W g f e = ( comp-equiv-Cyclic-Type k X Z W g (comp-equiv-Cyclic-Type k X Y Z f e)) ( refl-htpy) +``` +### Unit laws for composition of equivalences of cyclic types + +```agda module _ {l1 l2 : Level} (k : ℕ) (X : Cyclic-Type l1 k) (Y : Cyclic-Type l2 k) (e : equiv-Cyclic-Type k X Y) @@ -341,6 +364,15 @@ module _ ( comp-equiv-Cyclic-Type k X X Y e (id-equiv-Cyclic-Type k X)) ( e) ( refl-htpy) +``` + +### Inverse laws for equivalences of cyclic types + +```agda +module _ + {l1 l2 : Level} (k : ℕ) (X : Cyclic-Type l1 k) (Y : Cyclic-Type l2 k) + (e : equiv-Cyclic-Type k X Y) + where left-inverse-law-comp-equiv-Cyclic-Type : Id @@ -361,7 +393,11 @@ module _ ( comp-equiv-Cyclic-Type k Y X Y e (inv-equiv-Cyclic-Type k X Y e)) ( id-equiv-Cyclic-Type k Y) ( is-section-map-inv-equiv (equiv-equiv-Cyclic-Type k X Y e)) +``` +### Any two cyclic types of order `k` are merely equal + +```agda mere-eq-Cyclic-Type : {l : Level} (k : ℕ) (X Y : Cyclic-Type l k) → mere-eq X Y mere-eq-Cyclic-Type k X Y = apply-universal-property-trunc-Prop @@ -376,19 +412,34 @@ mere-eq-Cyclic-Type k X Y = ( eq-equiv-Cyclic-Type k X Y ( comp-equiv-Cyclic-Type k X (ℤ-Mod-Cyclic-Type k) Y f ( inv-equiv-Cyclic-Type k (ℤ-Mod-Cyclic-Type k) X e))))) +``` +### The type of cyclic types of order `k` is `0`-connected + +```agda is-0-connected-Cyclic-Type : (k : ℕ) → is-0-connected (Cyclic-Type lzero k) is-0-connected-Cyclic-Type k = is-0-connected-mere-eq ( ℤ-Mod-Cyclic-Type k) ( mere-eq-Cyclic-Type k (ℤ-Mod-Cyclic-Type k)) +``` +### The higher group of cyclic types + +```agda ∞-group-Cyclic-Type : (k : ℕ) → ∞-Group (lsuc lzero) pr1 (∞-group-Cyclic-Type k) = Cyclic-Type-Pointed-Type k pr2 (∞-group-Cyclic-Type k) = is-0-connected-Cyclic-Type k +``` + +### Characterization of equality of cyclic types + +To show that a cyclic type `X` is equal to a standard cyclic type, it suffices +to construct a point in `X`. +```agda Eq-Cyclic-Type : (k : ℕ) → Cyclic-Type lzero k → UU lzero Eq-Cyclic-Type k X = type-Cyclic-Type k X @@ -589,7 +640,11 @@ is-set-type-Ω-Cyclic-Type k = ( ℤ-Mod k) ( equiv-compute-Ω-Cyclic-Type k) ( is-set-ℤ-Mod k) +``` + +### The concrete group of cyclic types +```agda concrete-group-Cyclic-Type : (k : ℕ) → Concrete-Group (lsuc lzero) pr1 (concrete-group-Cyclic-Type k) = ∞-group-Cyclic-Type k @@ -616,6 +671,18 @@ iso-Ω-Cyclic-Type-Group k = ( equiv-Ω-Cyclic-Type-Group k) ``` +### Reduction of a cyclic type to a linear ordering, given an element + +```agda +module _ + {l1 : Level} (k : ℕ) (X : Cyclic-Type l1 k) (x : type-Cyclic-Type k X) + where + + leq-Cyclic-Type : + (y z : type-Cyclic-Type k X) → UU {!!} + leq-Cyclic-Type y z = leq-Fin k {!equiv-compute-Ω-Cyclic-Type k!} {!!} +``` + ## See also ### Table of files related to cyclic types, groups, and rings diff --git a/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md b/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md index 0f3dc73a32..80d8f95d4f 100644 --- a/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md +++ b/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md @@ -116,7 +116,7 @@ module _ (x : type-𝔽 A) → (y : type-𝔽 A) → is-finite (rel-Decidable-Relation R x y) is-finite-relation-Decidable-Relation-𝔽 x y = unit-trunc-Prop - ( count-Decidable-Prop + ( count-is-decidable-Prop ( relation-Decidable-Relation R x y) ( is-decidable-Decidable-Relation R x y)) diff --git a/src/univalent-combinatorics/decidable-propositions.lagda.md b/src/univalent-combinatorics/decidable-propositions.lagda.md index e5a046d04b..5d1ed4d53c 100644 --- a/src/univalent-combinatorics/decidable-propositions.lagda.md +++ b/src/univalent-combinatorics/decidable-propositions.lagda.md @@ -26,6 +26,16 @@ open import univalent-combinatorics.standard-finite-types
+## Idea + +We prove several properties of +[decidable propositions](foundation.decidable-propositions.md) and the type of +all decidable propositions involving +[countings](univalent-combinatorics.counting.md) and +[finiteness](univalent-combinatorics.finite-types.md). + +## Properties + ### Propositions have countings if and only if they are decidable ```agda @@ -42,12 +52,12 @@ count-is-decidable-is-prop H (inl x) = count-is-contr (is-proof-irrelevant-is-prop H x) count-is-decidable-is-prop H (inr f) = count-is-empty f -count-Decidable-Prop : +count-is-decidable-type-Prop : {l1 : Level} (P : Prop l1) → is-decidable (type-Prop P) → count (type-Prop P) -count-Decidable-Prop P (inl p) = +count-is-decidable-type-Prop P (inl p) = count-is-contr (is-proof-irrelevant-is-prop (is-prop-type-Prop P) p) -count-Decidable-Prop P (inr f) = count-is-empty f +count-is-decidable-type-Prop P (inr f) = count-is-empty f ``` ### We can count the elements of an identity type of a type that has decidable equality @@ -55,7 +65,7 @@ count-Decidable-Prop P (inr f) = count-is-empty f ```agda cases-count-eq : {l : Level} {X : UU l} (d : has-decidable-equality X) {x y : X} - (e : is-decidable (Id x y)) → count (Id x y) + (e : is-decidable (x ＝ y)) → count (x ＝ y) cases-count-eq d {x} {y} (inl p) = count-is-contr ( is-proof-irrelevant-is-prop (is-set-has-decidable-equality d x y) p) @@ -63,12 +73,12 @@ cases-count-eq d (inr f) = count-is-empty f count-eq : - {l : Level} {X : UU l} → has-decidable-equality X → (x y : X) → count (Id x y) + {l : Level} {X : UU l} → has-decidable-equality X → (x y : X) → count (x ＝ y) count-eq d x y = cases-count-eq d (d x y) cases-number-of-elements-count-eq' : {l : Level} {X : UU l} {x y : X} → - is-decidable (Id x y) → ℕ + is-decidable (x ＝ y) → ℕ cases-number-of-elements-count-eq' (inl p) = 1 cases-number-of-elements-count-eq' (inr f) = 0 @@ -79,18 +89,16 @@ number-of-elements-count-eq' d x y = cases-number-of-elements-count-eq : {l : Level} {X : UU l} (d : has-decidable-equality X) {x y : X} - (e : is-decidable (Id x y)) → - Id - ( number-of-elements-count (cases-count-eq d e)) - ( cases-number-of-elements-count-eq' e) + (e : is-decidable (x ＝ y)) → + number-of-elements-count (cases-count-eq d e) ＝ + cases-number-of-elements-count-eq' e cases-number-of-elements-count-eq d (inl p) = refl cases-number-of-elements-count-eq d (inr f) = refl -abstract - number-of-elements-count-eq : - {l : Level} {X : UU l} (d : has-decidable-equality X) (x y : X) → - Id ( number-of-elements-count (count-eq d x y)) - ( number-of-elements-count-eq' d x y) - number-of-elements-count-eq d x y = - cases-number-of-elements-count-eq d (d x y) +number-of-elements-count-eq : + {l : Level} {X : UU l} (d : has-decidable-equality X) (x y : X) → + number-of-elements-count (count-eq d x y) ＝ + number-of-elements-count-eq' d x y +number-of-elements-count-eq d x y = + cases-number-of-elements-count-eq d (d x y) ``` diff --git a/src/univalent-combinatorics/morphisms-cyclic-types.lagda.md b/src/univalent-combinatorics/morphisms-cyclic-types.lagda.md new file mode 100644 index 0000000000..b561f3daa1 --- /dev/null +++ b/src/univalent-combinatorics/morphisms-cyclic-types.lagda.md @@ -0,0 +1,84 @@ +# Morphisms of cyclic types + +```agda +{-# OPTIONS --allow-unsolved-metas #-} + +module univalent-combinatorics.morphisms-cyclic-types where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.function-types +open import foundation.universe-levels + +open import univalent-combinatorics.cyclic-types +``` + +
+ +## Idea + +A **morphism of [cyclic types](univalent-combinatorics.cyclic-types.md)** from a +cyclic type `(X,f)` of order `n` to a cyclic type `(Y,g)` of order `m` consists +of a map `h : X → Y` and a map `d : X → ℕ` where the value `d x : ℕ` is the +number of times `h` winds around the cyclic type `(Y,g)` before stepping from +the value `h x` to the value `h (f x)`. + +## Definitions + +### Morphisms of cyclic types + +```agda +module _ + {l1 l2 : Level} (m n : ℕ) (X : Cyclic-Type l1 m) (Y : Cyclic-Type l2 n) + where + + hom-Cyclic-Type : UU (l1 ⊔ l2) + hom-Cyclic-Type = + ( type-Cyclic-Type m X → type-Cyclic-Type n Y) × + ( type-Cyclic-Type m X → ℕ) + + module _ + (f : hom-Cyclic-Type) + where + + map-hom-Cyclic-Type : type-Cyclic-Type m X → type-Cyclic-Type n Y + map-hom-Cyclic-Type = pr1 f + + degree-at-value-hom-Cyclic-Type : type-Cyclic-Type m X → ℕ + degree-at-value-hom-Cyclic-Type = pr2 f +``` + +### Identity morphisms of cyclic types + +```agda +module _ + {l1 : Level} (m : ℕ) (X : Cyclic-Type l1 m) + where + + id-hom-Cyclic-Type : hom-Cyclic-Type m m X X + pr1 id-hom-Cyclic-Type = id + pr2 id-hom-Cyclic-Type x = 0 +``` + +### Composition of morphisms of cyclic types + +```agda +module _ + {l1 l2 l3 : Level} (l m n : ℕ) + (X : Cyclic-Type l1 l) + (Y : Cyclic-Type l2 m) + (Z : Cyclic-Type l3 n) + where + + comp-hom-Cyclic-Type : + hom-Cyclic-Type m n Y Z → hom-Cyclic-Type l m X Y → hom-Cyclic-Type l n X Z + pr1 (comp-hom-Cyclic-Type g f) = + map-hom-Cyclic-Type m n Y Z g ∘ map-hom-Cyclic-Type l m X Y f + pr2 (comp-hom-Cyclic-Type g f) = {!!} +``` diff --git a/src/univalent-combinatorics/omega-finite-types.lagda.md b/src/univalent-combinatorics/omega-finite-types.lagda.md new file mode 100644 index 0000000000..042b51ba0f --- /dev/null +++ b/src/univalent-combinatorics/omega-finite-types.lagda.md @@ -0,0 +1,72 @@ +# ω-Finite types + +```agda +module univalent-combinatorics.omega-finite-types where +``` + +
Imports + +```agda +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.unit-type +open import foundation.universe-levels + +open import synthetic-homotopy-theory.pushouts +``` + +
+ +## Idea + +The subuniverse of **ω-finite type** is the least subuniverse containing `∅`, +`𝟙`, and is closed under pushouts. The category of ω-finite types has +coproducts, cartesian products, and pushouts, but is not closed under pullbacks, +truncations, retracts, exponents, dependent products, quotients of segal +groupoids. + +The notion of ω-finite types was introduced by Mathieu Anel during the _Beyond +Finite Sets_ workshop in Copenhagen, on May 15th 2023. + +## Definition + +### The predicate of being ω-finite + +```agda +data ω-finite-structure : UU lzero → UU (lsuc lzero) where + ω-finite-structure-empty : ω-finite-structure empty + ω-finite-structure-unit : ω-finite-structure unit + ω-finite-structure-pushout : + {S : UU lzero} {A : UU lzero} {B : UU lzero} → + (f : S → A) (g : S → B) → + ω-finite-structure S → + ω-finite-structure A → + ω-finite-structure B → + ω-finite-structure (pushout f g) + +is-ω-finite-Prop : UU lzero → Prop (lsuc lzero) +is-ω-finite-Prop A = trunc-Prop (ω-finite-structure A) + +is-ω-finite : UU lzero → UU (lsuc lzero) +is-ω-finite X = type-Prop (is-ω-finite-Prop X) +``` + +### The type of ω-finite types + +```agda +ω-Finite-Type : UU (lsuc lzero) +ω-Finite-Type = Σ (UU lzero) is-ω-finite + +module _ + (X : ω-Finite-Type) + where + + type-ω-Finite-Type : UU lzero + type-ω-Finite-Type = pr1 X + + is-ω-finite-ω-Finite-Type : is-ω-finite type-ω-Finite-Type + is-ω-finite-ω-Finite-Type = pr2 X +``` diff --git a/src/univalent-combinatorics/reduced-1-bordism-category.lagda.md b/src/univalent-combinatorics/reduced-1-bordism-category.lagda.md new file mode 100644 index 0000000000..587687862f --- /dev/null +++ b/src/univalent-combinatorics/reduced-1-bordism-category.lagda.md @@ -0,0 +1,255 @@ +# The reduced 1-bordism category + +```agda +{-# OPTIONS --allow-unsolved-metas #-} + +module univalent-combinatorics.reduced-1-bordism-category where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.contractible-maps +open import foundation.contractible-types +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.functoriality-coproduct-types +open import foundation.identity-types +open import foundation.transport-along-identifications +open import foundation.type-arithmetic-coproduct-types +open import foundation.universe-levels + +open import graph-theory.directed-graphs +open import graph-theory.walks-directed-graphs + +open import univalent-combinatorics.finite-types +``` + +
+ +## Idea + +The reduced `1`-bordism category is the category of 1-bordisms where cycles are +ignored. + +## Definition + +### Objects in the reduced `1`-bordism category + +```agda +object-Reduced-1-Bordism : UU (lsuc lzero) +object-Reduced-1-Bordism = 𝔽 lzero × 𝔽 lzero + +positive-finite-type-object-Reduced-1-Bordism : + object-Reduced-1-Bordism → 𝔽 lzero +positive-finite-type-object-Reduced-1-Bordism = pr1 + +positive-type-object-Reduced-1-Bordism : + object-Reduced-1-Bordism → UU lzero +positive-type-object-Reduced-1-Bordism = + type-𝔽 ∘ positive-finite-type-object-Reduced-1-Bordism + +negative-finite-type-object-Reduced-1-Bordism : + object-Reduced-1-Bordism → 𝔽 lzero +negative-finite-type-object-Reduced-1-Bordism = pr2 + +negative-type-object-Reduced-1-Bordism : + object-Reduced-1-Bordism → UU lzero +negative-type-object-Reduced-1-Bordism = + type-𝔽 ∘ negative-finite-type-object-Reduced-1-Bordism +``` + +### Morphisms in the reduced `1`-bordism category + +```agda +hom-Reduced-1-Bordism : + (X Y : object-Reduced-1-Bordism) → UU lzero +hom-Reduced-1-Bordism X Y = + ( positive-type-object-Reduced-1-Bordism X + + negative-type-object-Reduced-1-Bordism Y) ≃ + ( positive-type-object-Reduced-1-Bordism Y + + negative-type-object-Reduced-1-Bordism X) +``` + +### Identity morphisms in the reduced `1`-bordism category + +```agda +id-hom-Reduced-1-Bordism : + (X : object-Reduced-1-Bordism) → hom-Reduced-1-Bordism X X +id-hom-Reduced-1-Bordism X = id-equiv +``` + +### Composition of morphisms in the reduced `1`-bordism category + +Composition of morphisms `g : (B⁺, B⁻) → (C⁺ , C⁻)` and +`f : (A⁺ , A⁻) → (B⁺, B⁻)` of reduced `1`-bordisms is defined via the sequence +of equivalences + +```text + (A⁺ ⊔ C⁻) ⊔ B⁻ ≃ (A⁺ ⊔ B⁻) ⊔ C⁻ + ≃ (B⁺ ⊔ A⁻) ⊔ C⁻ + ≃ (B⁺ ⊔ C⁻) ⊔ A⁻ + ≃ (C⁺ ⊔ B⁻) ⊔ A⁻ + ≃ (C⁺ ⊔ A⁻) ⊔ B⁻ +``` + +Call the composite equivalence `φ`. Then `φ` induces a directed graph on the +nods `(A⁺ ⊔ C⁻) ⊔ ((C⁺ ⊔ A⁻) ⊔ B⁻)` with the edge relation defined by + +```text + e₁ x : edge (inl x) (φ (inl x)) + e₂ b : edge (inr (inr b)) (φ (inr b)) +``` + +```agda +module _ + {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {Z : 𝔽 l3} + (φ : (X + type-𝔽 Z) ≃ (Y + type-𝔽 Z)) + where + + node-equiv-left-equiv-coprod : UU (l1 ⊔ l2 ⊔ l3) + node-equiv-left-equiv-coprod = X + (Y + type-𝔽 Z) + + data edge-equiv-left-equiv-coprod : + (u v : node-equiv-left-equiv-coprod) → UU (l1 ⊔ l2 ⊔ l3) + where + edge-to-value-equiv-left-equiv-coprod : + (x : X) → + edge-equiv-left-equiv-coprod (inl x) (inr (map-equiv φ (inl x))) + edge-right-summand-equiv-left-equiv-coprod : + (z : type-𝔽 Z) → + edge-equiv-left-equiv-coprod (inr (inr z)) (inr (map-equiv φ (inr z))) + + directed-graph-equiv-left-equiv-coprod : + Directed-Graph (l1 ⊔ l2 ⊔ l3) (l1 ⊔ l2 ⊔ l3) + pr1 directed-graph-equiv-left-equiv-coprod = + node-equiv-left-equiv-coprod + pr2 directed-graph-equiv-left-equiv-coprod = + edge-equiv-left-equiv-coprod + + direct-successor-equiv-left-equiv-coprod : + (x : X) → + direct-successor-Directed-Graph + ( directed-graph-equiv-left-equiv-coprod) + ( inl x) + pr1 (direct-successor-equiv-left-equiv-coprod x) = inr (map-equiv φ (inl x)) + pr2 (direct-successor-equiv-left-equiv-coprod x) = + edge-to-value-equiv-left-equiv-coprod x + + contraction-direct-successor-equiv-left-equiv-coprod : + (x : X) + ( s : + direct-successor-Directed-Graph + ( directed-graph-equiv-left-equiv-coprod) + ( inl x)) → + direct-successor-equiv-left-equiv-coprod x ＝ s + contraction-direct-successor-equiv-left-equiv-coprod x + ( ._ , edge-to-value-equiv-left-equiv-coprod .x) = + refl + + unique-direct-successor-equiv-left-equiv-coprod : + (x : X) → + is-contr + ( direct-successor-Directed-Graph + ( directed-graph-equiv-left-equiv-coprod) + ( inl x)) + pr1 (unique-direct-successor-equiv-left-equiv-coprod x) = + direct-successor-equiv-left-equiv-coprod x + pr2 (unique-direct-successor-equiv-left-equiv-coprod x) = + contraction-direct-successor-equiv-left-equiv-coprod x + + cases-direct-predecessor-equiv-left-equiv-coprod : + (y : Y) → + ( Σ X (λ x → map-equiv φ (inl x) ＝ inl y) + + Σ (type-𝔽 Z) (λ z → map-equiv φ (inr z) ＝ inl y)) → + direct-predecessor-Directed-Graph + ( directed-graph-equiv-left-equiv-coprod) + ( inr (inl y)) + pr1 (cases-direct-predecessor-equiv-left-equiv-coprod y (inl (x , p))) = + inl x + pr2 (cases-direct-predecessor-equiv-left-equiv-coprod y (inl (x , p))) = + tr + ( edge-equiv-left-equiv-coprod (inl x)) + ( ap inr p) + ( edge-to-value-equiv-left-equiv-coprod x) + pr1 (cases-direct-predecessor-equiv-left-equiv-coprod y (inr (z , p))) = + inr (inr z) + pr2 (cases-direct-predecessor-equiv-left-equiv-coprod y (inr (z , p))) = + tr + ( edge-equiv-left-equiv-coprod (inr (inr z))) + ( ap inr p) + ( edge-right-summand-equiv-left-equiv-coprod z) + + direct-predecessor-equiv-left-equiv-coprod : + (y : Y) → + direct-predecessor-Directed-Graph + ( directed-graph-equiv-left-equiv-coprod) + ( inr (inl y)) + direct-predecessor-equiv-left-equiv-coprod y = + cases-direct-predecessor-equiv-left-equiv-coprod y + ( map-right-distributive-Σ-coprod X + ( type-𝔽 Z) + ( λ u → map-equiv φ u ＝ inl y) + ( center (is-contr-map-is-equiv (is-equiv-map-equiv φ) (inl y)))) + + cases-contraction-direct-predecessor-equiv-left-equiv-coprod : + ( y : Y) → + ( d : + Σ X (λ x → map-equiv φ (inl x) ＝ inl y) + + Σ (type-𝔽 Z) (λ z → map-equiv φ (inr z) ＝ inl y)) + ( p : + direct-predecessor-Directed-Graph + ( directed-graph-equiv-left-equiv-coprod) + ( inr (inl y))) → + cases-direct-predecessor-equiv-left-equiv-coprod y d ＝ p + cases-contraction-direct-predecessor-equiv-left-equiv-coprod y + ( inl (x , q)) (inl x' , e) = + {!!} + {- + ap + ( pr1) + ( ( eq-is-contr (is-contr-map-is-equiv (is-equiv-map-equiv φ) (inl y))) + { inl x , q} + { inl x' , ?}) -} + cases-contraction-direct-predecessor-equiv-left-equiv-coprod y + ( inl (x , q)) (inr n , e) = + {!!} + cases-contraction-direct-predecessor-equiv-left-equiv-coprod y + ( inr (z , q)) p = + {!!} + + unique-direct-predecessor-equiv-left-equiv-coprod : + (y : Y) → + is-contr + ( direct-predecessor-Directed-Graph + ( directed-graph-equiv-left-equiv-coprod) + ( inr (inl y))) + unique-direct-predecessor-equiv-left-equiv-coprod y = {!!} + + walk-equiv-left-equiv-coprod : + (x y : node-equiv-left-equiv-coprod) → UU (l1 ⊔ l2 ⊔ l3) + walk-equiv-left-equiv-coprod = + walk-Directed-Graph directed-graph-equiv-left-equiv-coprod + + walk-across-equiv-left-equiv-coprod : + (x : X) → + Σ Y (λ y → edge-equiv-left-equiv-coprod (inl x) (inr (inl y))) + walk-across-equiv-left-equiv-coprod x = {!!} +``` + +In this graph, there is for each `x : A⁺ ⊔ C⁻` a unique element `y : C⁺ ⊔ A⁻` +equipped with a walk from `inl x` to `inl (inr y)`. This determines an +equivalence `A⁺ ⊔ C⁻ ≃ C⁺ ⊔ A⁻` which we use to define the composite `g ∘ f`. + +```agda +comp-hom-Reduced-1-Bordism : + {X Y Z : object-Reduced-1-Bordism} → + hom-Reduced-1-Bordism Y Z → hom-Reduced-1-Bordism X Y → + hom-Reduced-1-Bordism X Z +comp-hom-Reduced-1-Bordism g f = {!!} +``` diff --git a/src/univalent-combinatorics/symmetric-operations.lagda.md b/src/univalent-combinatorics/symmetric-operations.lagda.md new file mode 100644 index 0000000000..256b4f40bf --- /dev/null +++ b/src/univalent-combinatorics/symmetric-operations.lagda.md @@ -0,0 +1,56 @@ +# Symmetric operations on finite sets + +```agda +module univalent-combinatorics.symmetric-operations where + +open import foundation.symmetric-operations public +``` + +
Imports + +```agda +open import foundation.universe-levels + +open import univalent-combinatorics.dependent-function-types +open import univalent-combinatorics.dependent-pair-types +open import univalent-combinatorics.equality-finite-types +open import univalent-combinatorics.finite-types +open import univalent-combinatorics.function-types +``` + +
+ +## Idea + +The type of [symmetric operations](foundation.symmetric-operations.md) from one +[finite type](univalent-combinatorics.finite-types.md) into another is finite. + +## Properties + +### The type of symmetric operations from one finite type into another is finite + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + is-finite-symmetric-operation : + is-finite A → is-finite B → is-finite (symmetric-operation A B) + is-finite-symmetric-operation H K = + is-finite-equiv' + ( compute-symmetric-operation-Set A (B , is-set-is-finite K)) + ( is-finite-Σ + ( is-finite-function-type H (is-finite-function-type H K)) + ( λ f → + is-finite-Π H + ( λ x → + is-finite-Π H + ( λ y → is-finite-eq (has-decidable-equality-is-finite K))))) + +symmetric-operation-𝔽 : + {l1 l2 : Level} → 𝔽 l1 → 𝔽 l2 → 𝔽 (lsuc lzero ⊔ l1 ⊔ l2) +pr1 (symmetric-operation-𝔽 A B) = + symmetric-operation (type-𝔽 A) (type-𝔽 B) +pr2 (symmetric-operation-𝔽 A B) = + is-finite-symmetric-operation (is-finite-type-𝔽 A) (is-finite-type-𝔽 B) +``` diff --git a/src/univalent-combinatorics/unordered-pairs-of-elements-finite-types.lagda.md b/src/univalent-combinatorics/unordered-pairs-of-elements-finite-types.lagda.md new file mode 100644 index 0000000000..1849a0b75e --- /dev/null +++ b/src/univalent-combinatorics/unordered-pairs-of-elements-finite-types.lagda.md @@ -0,0 +1,51 @@ +# Unordered pairs of elements in finite types + +```agda +module univalent-combinatorics.unordered-pairs-of-elements-finite-types where + +open import foundation.unordered-pairs public +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.universe-levels + +open import univalent-combinatorics.finite-types +open import univalent-combinatorics.function-types +open import univalent-combinatorics.pi-finite-types +``` + +
+ +## Idea + +The type of [unordered pairs](foundation.unordered-pairs.md) of elements in a +[finite type](univalent-combinatorics.finite-types.md) is a +[π-finite type](univalent-combinatorics.pi-finite-types.md). + +Note: The type of unordered pairs in a π-finite type is also π-finite. However, +we haven't shown yet that π-finite types are closed under dependent products. + +## Properties + +### The type of unordered pairs of elements in a finite type is π-finite + +```agda +module _ + {l1 : Level} (X : 𝔽 l1) + where + + is-π-finite-unordered-pair-𝔽 : + (k : ℕ) → is-π-finite k (unordered-pair (type-𝔽 X)) + is-π-finite-unordered-pair-𝔽 k = + is-π-finite-Σ k + ( is-π-finite-UU-Fin (succ-ℕ k) 2) + ( λ I → + is-π-finite-is-finite k + ( is-finite-function-type + ( is-finite-has-cardinality 2 (has-cardinality-type-UU-Fin 2 I)) + ( is-finite-type-𝔽 X))) +```