From 7ae01a146775d3a08b74b0e62308316a0cd01105 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Mon, 15 May 2023 11:05:26 +0200
Subject: [PATCH 01/23] omega finite types

---
 src/univalent-combinatorics.lagda.md          |  1 +
 .../omega-finite-types.lagda.md               | 72 +++++++++++++++++++
 2 files changed, 73 insertions(+)
 create mode 100644 src/univalent-combinatorics/omega-finite-types.lagda.md

diff --git a/src/univalent-combinatorics.lagda.md b/src/univalent-combinatorics.lagda.md
index 9764775769..0c902087a0 100644
--- a/src/univalent-combinatorics.lagda.md
+++ b/src/univalent-combinatorics.lagda.md
@@ -76,6 +76,7 @@ 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.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
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
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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
+```

From eb4b4508f9613b6c2adb39afbb1f616378505801 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Tue, 16 May 2023 14:36:03 +0200
Subject: [PATCH 02/23] file for reduced 1-bordsim category

---
 .../cyclic-types.lagda.md                     |   9 ++
 .../reduced-1-bordism-category.lagda.md       | 141 ++++++++++++++++++
 2 files changed, 150 insertions(+)
 create mode 100644 src/univalent-combinatorics/reduced-1-bordism-category.lagda.md

diff --git a/src/univalent-combinatorics/cyclic-types.lagda.md b/src/univalent-combinatorics/cyclic-types.lagda.md
index 015c206e87..726371098e 100644
--- a/src/univalent-combinatorics/cyclic-types.lagda.md
+++ b/src/univalent-combinatorics/cyclic-types.lagda.md
@@ -582,3 +582,12 @@ iso-Ω-Cyclic-Type-Group k =
     ( ℤ-Mod-Group k)
     ( equiv-Ω-Cyclic-Type-Group k)
 ```
+
+### The category of cyclic types
+
+```agda
+hom-Cyclic-Type :
+  {l1 l2 : Level} (m n : ℕ) (X : Cyclic-Type l1 m) (Y : Cyclic-Type l2 n) →
+  UU {!!}
+hom-Cyclic-Type m n X Y = {!!}
+```
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..c13dda7451
--- /dev/null
+++ b/src/univalent-combinatorics/reduced-1-bordism-category.lagda.md
@@ -0,0 +1,141 @@
+# The reduced 1-bordism category
+
+```agda
+module univalent-combinatorics.reduced-1-bordism-category where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.empty-types
+open import foundation.equivalences
+open import foundation.functions
+open import foundation.universe-levels
+
+open import graph-theory.directed-graphs
+open import graph-theory.walks-directed-graphs
+
+open import univalent-combinatorics.finite-types
+```
+
+</details>
+
+## 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
+
+  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 = {!!}
+```

From 2c1a319060979abbb823069c6fc977d5530723fb Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Tue, 16 May 2023 14:36:19 +0200
Subject: [PATCH 03/23] file for cyclically ordered sets

---
 ...egory-of-cyclically-ordered-types.lagda.md | 23 +++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 src/univalent-combinatorics/category-of-cyclically-ordered-types.lagda.md

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..925a292b72
--- /dev/null
+++ b/src/univalent-combinatorics/category-of-cyclically-ordered-types.lagda.md
@@ -0,0 +1,23 @@
+# The category of cyclically ordered types
+
+```agda
+module univalent-combinatorics.category-of-cyclically-ordered-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+```
+
+</details>
+
+## 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`.

From 33ae514a1e3d17474085f4358537418d81acb156 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 18 May 2023 12:09:12 +0200
Subject: [PATCH 04/23] work

---
 .../reduced-1-bordism-category.lagda.md       | 93 ++++++++++++++++++-
 1 file changed, 92 insertions(+), 1 deletion(-)

diff --git a/src/univalent-combinatorics/reduced-1-bordism-category.lagda.md b/src/univalent-combinatorics/reduced-1-bordism-category.lagda.md
index c13dda7451..b8151b7fad 100644
--- a/src/univalent-combinatorics/reduced-1-bordism-category.lagda.md
+++ b/src/univalent-combinatorics/reduced-1-bordism-category.lagda.md
@@ -8,11 +8,16 @@ module univalent-combinatorics.reduced-1-bordism-category where
 
 ```agda
 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.functions
+open import foundation.functoriality-coproduct-types
+open import foundation.identity-types
+open import foundation.type-arithmetic-coproduct-types
 open import foundation.universe-levels
 
 open import graph-theory.directed-graphs
@@ -119,6 +124,92 @@ module _
   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 =
@@ -127,7 +218,7 @@ module _
   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 = ?
+  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`.

From 5e878fd36fcd70055303720e1e9d4b48862e88c0 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 18 May 2023 12:09:52 +0200
Subject: [PATCH 05/23] work

---
 ...s-of-elements-commutative-monoids.lagda.md | 32 +++++++++++++++++
 .../rational-commutative-monoids.lagda.md     | 35 +++++++++++++++++++
 2 files changed, 67 insertions(+)
 create mode 100644 src/group-theory/powers-of-elements-commutative-monoids.lagda.md
 create mode 100644 src/group-theory/rational-commutative-monoids.lagda.md

diff --git a/src/group-theory/powers-of-elements-commutative-monoids.lagda.md b/src/group-theory/powers-of-elements-commutative-monoids.lagda.md
new file mode 100644
index 0000000000..69e8db8b09
--- /dev/null
+++ b/src/group-theory/powers-of-elements-commutative-monoids.lagda.md
@@ -0,0 +1,32 @@
+# Powers of elements in commutative monoids
+
+```agda
+module group-theory.powers-of-elements-commutative-monoids where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.universe-levels
+
+open import group-theory.commutative-monoids
+```
+
+</details>
+
+## Idea
+
+Consider an element `x` in a [commutative monoid](group-theory.commutative-monoids.md) and a [natural number](elementary-number-theory.natural-numbers.md) `n : ℕ`. The `n`-th **power** of `x` is the `n` times iterated product of `x` with itself.
+
+## Definition
+
+```agda
+power-Commutative-Monoid :
+  {l : Level} (M : Commutative-Monoid l) → ℕ → type-Commutative-Monoid M → type-Commutative-Monoid M
+power-Commutative-Monoid M zero-ℕ x = unit-Commutative-Monoid M
+power-Commutative-Monoid M (succ-ℕ zero-ℕ) x = x
+power-Commutative-Monoid M (succ-ℕ (succ-ℕ n)) x =
+  mul-Commutative-Monoid M (power-Commutative-Monoid M (succ-ℕ n) x) x
+```
diff --git a/src/group-theory/rational-commutative-monoids.lagda.md b/src/group-theory/rational-commutative-monoids.lagda.md
new file mode 100644
index 0000000000..403e4b76e3
--- /dev/null
+++ b/src/group-theory/rational-commutative-monoids.lagda.md
@@ -0,0 +1,35 @@
+# Rational commutative monoids
+
+```agda
+module group-theory.rational-commutative-monoids where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.equivalences
+open import foundation.universe-levels
+
+open import group-theory.commutative-monoids
+open import group-theory.powers-of-elements-commutative-monoids
+```
+
+</details>
+
+## Idea
+
+A **rational commutative monoid** is a [commutative monoid](group-theory.commutative-monoids.md) `(M,0,+)` in which the map `x ↦ nx` is invertible for every natural number `n`.
+
+Note: since we usually write commutative monoids multiplicatively, the condition that a commutative monoid is rational is that the map `x ↦ xⁿ` is invertible for every natural number `n`.
+
+## Definition
+
+### The predicate of being a rational commutative monoid
+
+```agda
+is-rational-Commutative-Monoid : {l : Level} → Commutative-Monoid l → UU l
+is-rational-Commutative-Monoid M =
+  (n : ℕ) → is-equiv (power-Commutative-Monoid M n)
+```

From 23ac890c54a9990c87e0c71e12a2c2592ca9b8e2 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sat, 20 May 2023 18:30:31 +0200
Subject: [PATCH 06/23] demonstration

---
 .../decidable-propositions.lagda.md           |   4 +
 src/foundation/symmetric-operations.lagda.md  | 166 +++++++++++++++++-
 src/foundation/unordered-pairs.lagda.md       |  27 ++-
 ...a.md => finite-undirected-graphs.lagda.md} |  48 ++++-
 .../neighbors-undirected-graphs.lagda.md      |   6 +-
 src/trees/finite-undirected-trees.lagda.md    | 142 +++++++++++++++
 src/trees/undirected-trees.lagda.md           |  11 ++
 .../cyclic-types.lagda.md                     |  67 ++++++-
 .../decidable-propositions.lagda.md           |  33 ++--
 .../morphisms-cyclic-types.lagda.md           |  78 ++++++++
 .../symmetric-operations.lagda.md             |  53 ++++++
 ...ed-pairs-of-elements-finite-types.lagda.md |  48 +++++
 12 files changed, 653 insertions(+), 30 deletions(-)
 rename src/graph-theory/{finite-graphs.lagda.md => finite-undirected-graphs.lagda.md} (62%)
 create mode 100644 src/trees/finite-undirected-trees.lagda.md
 create mode 100644 src/univalent-combinatorics/morphisms-cyclic-types.lagda.md
 create mode 100644 src/univalent-combinatorics/symmetric-operations.lagda.md
 create mode 100644 src/univalent-combinatorics/unordered-pairs-of-elements-finite-types.lagda.md

diff --git a/src/foundation/decidable-propositions.lagda.md b/src/foundation/decidable-propositions.lagda.md
index 9f1152dba8..b6f46a1dc4 100644
--- a/src/foundation/decidable-propositions.lagda.md
+++ b/src/foundation/decidable-propositions.lagda.md
@@ -168,6 +168,10 @@ pr2 (iff-universes-Decidable-Prop l l' P) p =
 is-set-Decidable-Prop : {l : Level} → is-set (Decidable-Prop l)
 is-set-Decidable-Prop {l} =
   is-set-equiv bool equiv-bool-Decidable-Prop is-set-bool
+
+Decidable-Prop-Set : (l : Level) → Set (lsuc l)
+pr1 (Decidable-Prop-Set l) = Decidable-Prop l
+pr2 (Decidable-Prop-Set l) = is-set-Decidable-Prop
 ```
 
 ### Extensionality of decidable propositions
diff --git a/src/foundation/symmetric-operations.lagda.md b/src/foundation/symmetric-operations.lagda.md
index b58863b504..7f036ef7d6 100644
--- a/src/foundation/symmetric-operations.lagda.md
+++ b/src/foundation/symmetric-operations.lagda.md
@@ -1,14 +1,24 @@
 # Symmetric operations
 
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module foundation.symmetric-operations where
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.contractible-types
 open import foundation.equivalence-extensionality
+open import foundation.function-extensionality
+open import foundation.functions
 open import foundation.functoriality-coproduct-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.subtypes
 open import foundation.universal-property-propositional-truncation-into-sets
 open import foundation.unordered-pairs
 
@@ -54,14 +64,26 @@ module _
 
   is-commutative : (A → A → B) → UU (l1 ⊔ l2)
   is-commutative f = (x y : A) → f x y ＝ f y x
+
+is-commutative-Prop :
+  {l1 l2 : Level} {A : UU l1} (B : Set l2) → (A → A → type-Set B) → Prop (l1 ⊔ l2)
+is-commutative-Prop B f =
+  Π-Prop _ (λ x → Π-Prop _ (λ y → Id-Prop B (f x y) (f y x)))
 ```
 
 ### Commutative operations
 
 ```agda
-symmetric-operation :
-  {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (lsuc lzero ⊔ l1 ⊔ l2)
-symmetric-operation A B = unordered-pair A → B
+module _
+  {l1 l2 : Level} (A : UU l1) (B : UU l2)
+  where
+  
+  symmetric-operation : UU (lsuc lzero ⊔ l1 ⊔ l2)
+  symmetric-operation = unordered-pair A → B
+
+  map-symmetric-operation : symmetric-operation → A → A → B
+  map-symmetric-operation f x y =
+    f (standard-unordered-pair x y)
 ```
 
 ## Properties
@@ -141,3 +163,141 @@ module _
     p : Fin 2 → A
     p = pr2 (standard-unordered-pair x y)
 ```
+
+### Characterization of equality of symmetric operations into sets
+
+```agda
+module _
+  {l1 l2 : Level} (A : UU l1) (B : Set l2) (f : symmetric-operation A (type-Set B))
+  where
+
+  htpy-symmetric-operation-Set-Prop :
+    (g : symmetric-operation A (type-Set B)) → Prop (l1 ⊔ l2)
+  htpy-symmetric-operation-Set-Prop g =
+    Π-Prop A
+      ( λ x →
+        Π-Prop A
+          ( λ y →
+            Id-Prop B
+              ( map-symmetric-operation A (type-Set B) f x y)
+              ( map-symmetric-operation A (type-Set B) g x y)))
+
+  htpy-symmetric-operation-Set :
+    (g : symmetric-operation A (type-Set B)) → UU (l1 ⊔ l2)
+  htpy-symmetric-operation-Set g =
+    type-Prop (htpy-symmetric-operation-Set-Prop g)
+
+  center-total-htpy-symmetric-operation-Set :
+     Σ ( symmetric-operation A (type-Set B))
+       ( htpy-symmetric-operation-Set)
+  pr1 center-total-htpy-symmetric-operation-Set = f
+  pr2 center-total-htpy-symmetric-operation-Set x y = refl
+
+  contraction-total-htpy-symmetric-operation-Set :
+    ( t :
+      Σ ( symmetric-operation A (type-Set B))
+        ( htpy-symmetric-operation-Set)) →
+    center-total-htpy-symmetric-operation-Set ＝ t
+  contraction-total-htpy-symmetric-operation-Set (g , H) =
+    eq-type-subtype
+      htpy-symmetric-operation-Set-Prop
+      ( eq-htpy
+        ( λ p →
+          apply-universal-property-trunc-Prop
+            ( is-surjective-standard-unordered-pair p)
+            ( Id-Prop B (f p) (g p))
+            ( λ { (x , y , refl) → H x y})))
+
+  is-contr-total-htpy-symmetric-operation-Set :
+    is-contr
+      ( Σ ( symmetric-operation A (type-Set B))
+          ( htpy-symmetric-operation-Set))
+  pr1 is-contr-total-htpy-symmetric-operation-Set =
+    center-total-htpy-symmetric-operation-Set
+  pr2 is-contr-total-htpy-symmetric-operation-Set =
+    contraction-total-htpy-symmetric-operation-Set
+
+  htpy-eq-symmetric-operation-Set :
+    (g : symmetric-operation A (type-Set B)) →
+    (f ＝ g) → htpy-symmetric-operation-Set g
+  htpy-eq-symmetric-operation-Set g refl x y = refl
+
+  is-equiv-htpy-eq-symmetric-operation-Set :
+    (g : symmetric-operation A (type-Set B)) →
+    is-equiv (htpy-eq-symmetric-operation-Set g)
+  is-equiv-htpy-eq-symmetric-operation-Set =
+    fundamental-theorem-id
+      is-contr-total-htpy-symmetric-operation-Set
+      htpy-eq-symmetric-operation-Set
+      
+  extensionality-symmetric-operation-Set :
+    (g : symmetric-operation A (type-Set B)) →
+    (f ＝ g) ≃ htpy-symmetric-operation-Set g
+  pr1 (extensionality-symmetric-operation-Set g) =
+    htpy-eq-symmetric-operation-Set g
+  pr2 (extensionality-symmetric-operation-Set g) =
+    is-equiv-htpy-eq-symmetric-operation-Set g
+
+  eq-htpy-symmetric-operation-Set :
+    (g : symmetric-operation A (type-Set B)) →
+    htpy-symmetric-operation-Set g → (f ＝ g)
+  eq-htpy-symmetric-operation-Set g =
+    map-inv-equiv (extensionality-symmetric-operation-Set g)
+```
+
+### The type of commutative operations into a set is equivalent to the type of symmetric operations
+
+```agda
+module _
+  {l1 l2 : Level} (A : UU l1) (B : Set l2)
+  where
+
+  map-compute-symmetric-operation-Set :
+    symmetric-operation A (type-Set B) → Σ (A → A → type-Set B) is-commutative
+  pr1 (map-compute-symmetric-operation-Set f) = map-symmetric-operation A (type-Set B) f
+  pr2 (map-compute-symmetric-operation-Set f) = is-commutative-symmetric-operation f
+
+  map-inv-compute-symmetric-operation-Set :
+    Σ (A → A → type-Set B) is-commutative → symmetric-operation A (type-Set B)
+  map-inv-compute-symmetric-operation-Set (f , H) =
+    symmetric-operation-is-commutative B f H
+
+  issec-map-inv-compute-symmetric-operation-Set :
+    ( map-compute-symmetric-operation-Set ∘
+      map-inv-compute-symmetric-operation-Set) ~ id
+  issec-map-inv-compute-symmetric-operation-Set (f , H) =
+    eq-type-subtype
+      ( is-commutative-Prop B)
+      ( eq-htpy
+        ( λ x →
+          eq-htpy
+            ( λ y →
+              compute-symmetric-operation-is-commutative B f H x y)))
+
+  isretr-map-inv-compute-symmetric-operation-Set :
+    ( map-inv-compute-symmetric-operation-Set ∘
+      map-compute-symmetric-operation-Set) ~ id
+  isretr-map-inv-compute-symmetric-operation-Set g =
+    eq-htpy-symmetric-operation-Set A B
+      ( map-inv-compute-symmetric-operation-Set
+        ( map-compute-symmetric-operation-Set g))
+      ( g)
+      ( compute-symmetric-operation-is-commutative B
+        ( map-symmetric-operation A (type-Set B) g)
+        ( is-commutative-symmetric-operation g))
+
+  is-equiv-map-compute-symmetric-operation-Set :
+    is-equiv map-compute-symmetric-operation-Set
+  is-equiv-map-compute-symmetric-operation-Set =
+    is-equiv-has-inverse
+      map-inv-compute-symmetric-operation-Set
+      issec-map-inv-compute-symmetric-operation-Set
+      isretr-map-inv-compute-symmetric-operation-Set
+
+  compute-symmetric-operation-Set :
+    symmetric-operation A (type-Set B) ≃ Σ (A → A → type-Set B) is-commutative
+  pr1 compute-symmetric-operation-Set =
+    map-compute-symmetric-operation-Set
+  pr2 compute-symmetric-operation-Set =
+    is-equiv-map-compute-symmetric-operation-Set
+```
diff --git a/src/foundation/unordered-pairs.lagda.md b/src/foundation/unordered-pairs.lagda.md
index e4094152e8..1fcc16f79f 100644
--- a/src/foundation/unordered-pairs.lagda.md
+++ b/src/foundation/unordered-pairs.lagda.md
@@ -14,6 +14,7 @@ open import foundation.homotopies
 open import foundation.mere-equivalences
 open import foundation.propositional-truncations
 open import foundation.structure-identity-principle
+open import foundation.unit-type
 
 open import foundation-core.contractible-types
 open import foundation-core.coproduct-types
@@ -344,5 +345,29 @@ id-equiv-standard-unordered-pair x y =
 
 unordered-distinct-pair :
   {l : Level} (A : UU l) → UU (lsuc lzero ⊔ l)
-unordered-distinct-pair A = Σ (UU-Fin lzero 2) (λ X → pr1 X ↪ A)
+unordered-distinct-pair A =
+  Σ (UU-Fin lzero 2) (λ X → pr1 X ↪ A)
+```
+
+### Every unordered pair is merely equal to a standard unordered pair
+
+```agda
+is-surjective-standard-unordered-pair :
+  {l : Level} {A : UU l} (p : unordered-pair A) →
+  type-trunc-Prop
+    ( Σ A (λ x → Σ A (λ y → standard-unordered-pair x y ＝ p)))
+is-surjective-standard-unordered-pair (I , a) =
+  apply-universal-property-trunc-Prop
+    ( has-two-elements-type-2-Element-Type I)
+    ( trunc-Prop
+      ( Σ _ (λ x → Σ _ (λ y → standard-unordered-pair x y ＝ (I , a)))))
+    ( λ e →
+      unit-trunc-Prop
+        ( a (map-equiv e (zero-Fin 1)) ,
+          a (map-equiv e (one-Fin 1)) ,
+          eq-Eq-unordered-pair
+            ( standard-unordered-pair _ _)
+            ( I , a)
+            ( e)
+            ( λ { (inl (inr star)) → refl ; (inr star) → refl})))
 ```
diff --git a/src/graph-theory/finite-graphs.lagda.md b/src/graph-theory/finite-undirected-graphs.lagda.md
similarity index 62%
rename from src/graph-theory/finite-graphs.lagda.md
rename to src/graph-theory/finite-undirected-graphs.lagda.md
index dad45d2acb..6d78b59489 100644
--- a/src/graph-theory/finite-graphs.lagda.md
+++ b/src/graph-theory/finite-undirected-graphs.lagda.md
@@ -1,7 +1,7 @@
 # Finite graphs
 
 ```agda
-module graph-theory.finite-graphs where
+module graph-theory.finite-undirected-graphs where
 ```
 
 <details><summary>Imports</summary>
@@ -11,7 +11,11 @@ open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.fibers-of-maps
 open import foundation.functions
+open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
+open import foundation.propositions
+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
 
@@ -24,11 +28,36 @@ open import univalent-combinatorics.finite-types
 
 ## Idea
 
-A finite undirected graph consists of a finite set of vertices and a family of
-finite types of edges indexed by unordered pairs of vertices.
+A **finite undirected graph** consists of a [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.
 
 ## 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
@@ -65,6 +94,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/neighbors-undirected-graphs.lagda.md b/src/graph-theory/neighbors-undirected-graphs.lagda.md
index ab665b0df2..97a6a3421e 100644
--- a/src/graph-theory/neighbors-undirected-graphs.lagda.md
+++ b/src/graph-theory/neighbors-undirected-graphs.lagda.md
@@ -25,10 +25,12 @@ 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/trees/finite-undirected-trees.lagda.md b/src/trees/finite-undirected-trees.lagda.md
new file mode 100644
index 0000000000..ef4bd92298
--- /dev/null
+++ b/src/trees/finite-undirected-trees.lagda.md
@@ -0,0 +1,142 @@
+# Finite undirected trees
+
+```agda
+module trees.finite-undirected-trees where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.decidable-propositions
+open import foundation.dependent-pair-types
+open import foundation.functions
+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.finite-types
+open import univalent-combinatorics.pi-finite-types
+open import univalent-combinatorics.symmetric-operations
+```
+
+</details>
+
+## 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 ?
+```
+
+## Properties
+
+### The type of finite undirected trees of cardinality `n` is π-finite
+
+```agda
+is-π-finite-Undirected-Tree-of-cardinality :
+  (k n : ℕ) → is-π-finite k (Undirected-Tree-Of-Size lzero lzero n)
+is-π-finite-Undirected-Tree-of-cardinality 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 →
+          {!!}))
+```
diff --git a/src/trees/undirected-trees.lagda.md b/src/trees/undirected-trees.lagda.md
index c2423ff065..ff611d050e 100644
--- a/src/trees/undirected-trees.lagda.md
+++ b/src/trees/undirected-trees.lagda.md
@@ -37,6 +37,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/cyclic-types.lagda.md b/src/univalent-combinatorics/cyclic-types.lagda.md
index 726371098e..711a089c08 100644
--- a/src/univalent-combinatorics/cyclic-types.lagda.md
+++ b/src/univalent-combinatorics/cyclic-types.lagda.md
@@ -9,6 +9,7 @@ module univalent-combinatorics.cyclic-types where
 ```agda
 open import elementary-number-theory.addition-integers
 open import elementary-number-theory.groups-of-modular-arithmetic
+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
@@ -51,8 +52,8 @@ 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
+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
@@ -200,6 +201,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)
@@ -261,7 +264,11 @@ module _
     (e f : equiv-Cyclic-Type k X Y) → htpy-equiv-Cyclic-Type e f → Id 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) →
@@ -271,13 +278,21 @@ 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
 inv-equiv-Cyclic-Type k X Y =
   inv-equiv-Endo (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)
@@ -294,7 +309,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)
@@ -315,6 +334,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 ( comp-equiv-Cyclic-Type k X Y X (inv-equiv-Cyclic-Type k X Y e) e)
@@ -333,7 +361,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)
       ( issec-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
@@ -348,19 +380,33 @@ 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
 
@@ -556,7 +602,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
@@ -583,11 +633,14 @@ iso-Ω-Cyclic-Type-Group k =
     ( equiv-Ω-Cyclic-Type-Group k)
 ```
 
-### The category of cyclic types
+### Reduction of a cyclic type to a linear ordering, given an element
 
 ```agda
-hom-Cyclic-Type :
-  {l1 l2 : Level} (m n : ℕ) (X : Cyclic-Type l1 m) (Y : Cyclic-Type l2 n) →
-  UU {!!}
-hom-Cyclic-Type m n X Y = {!!}
+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!} {!!}
 ```
diff --git a/src/univalent-combinatorics/decidable-propositions.lagda.md b/src/univalent-combinatorics/decidable-propositions.lagda.md
index ad7a4a1548..4b2917dbcb 100644
--- a/src/univalent-combinatorics/decidable-propositions.lagda.md
+++ b/src/univalent-combinatorics/decidable-propositions.lagda.md
@@ -26,6 +26,12 @@ open import univalent-combinatorics.standard-finite-types
 
 </details>
 
+## 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 +48,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 +61,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 +69,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,17 +85,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)) →
+  (e : is-decidable (x ＝ y)) →
   Id ( 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..acf7ff317e
--- /dev/null
+++ b/src/univalent-combinatorics/morphisms-cyclic-types.lagda.md
@@ -0,0 +1,78 @@
+# Morphisms of cyclic types
+
+```agda
+module univalent-combinatorics.morphisms-cyclic-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.functions
+open import foundation.universe-levels
+
+open import univalent-combinatorics.cyclic-types
+```
+
+</details>
+
+## 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/symmetric-operations.lagda.md b/src/univalent-combinatorics/symmetric-operations.lagda.md
new file mode 100644
index 0000000000..5a90a3521d
--- /dev/null
+++ b/src/univalent-combinatorics/symmetric-operations.lagda.md
@@ -0,0 +1,53 @@
+# Symmetric operations on finite sets
+
+```agda
+module univalent-combinatorics.symmetric-operations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.symmetric-operations public
+
+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..69e5504cdb
--- /dev/null
+++ b/src/univalent-combinatorics/unordered-pairs-of-elements-finite-types.lagda.md
@@ -0,0 +1,48 @@
+# Unordered pairs of elements in finite types
+
+```agda
+module univalent-combinatorics.unordered-pairs-of-elements-finite-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.unordered-pairs public
+
+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
+```
+
+</details>
+
+## 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)))
+```

From 61796a3e0190360ed48d3cc2393279b1a0ad574b Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 14 Jun 2023 17:14:55 +0200
Subject: [PATCH 07/23] make pre-commit

---
 src/graph-theory.lagda.md                     |  1 +
 .../walks-finite-undirected-graphs.lagda.md   | 33 ++++++++++++++-----
 src/trees/finite-undirected-trees.lagda.md    |  3 +-
 3 files changed, 27 insertions(+), 10 deletions(-)

diff --git a/src/graph-theory.lagda.md b/src/graph-theory.lagda.md
index e95d5d5e2c..5d22b843ae 100644
--- a/src/graph-theory.lagda.md
+++ b/src/graph-theory.lagda.md
@@ -50,5 +50,6 @@ open import graph-theory.undirected-graphs public
 open import graph-theory.vertex-covers public
 open import graph-theory.voltage-graphs public
 open import graph-theory.walks-directed-graphs public
+open import graph-theory.walks-finite-undirected-graphs public
 open import graph-theory.walks-undirected-graphs public
 ```
diff --git a/src/graph-theory/walks-finite-undirected-graphs.lagda.md b/src/graph-theory/walks-finite-undirected-graphs.lagda.md
index 990e6f2dfd..2208223259 100644
--- a/src/graph-theory/walks-finite-undirected-graphs.lagda.md
+++ b/src/graph-theory/walks-finite-undirected-graphs.lagda.md
@@ -35,9 +35,16 @@ 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).
+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.
+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
 
@@ -47,7 +54,7 @@ Note that the type of walks in a finite undirected graph does not need to be [fi
 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-𝔽 =
@@ -145,14 +152,15 @@ module _
   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) 
+    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)
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  (x : vertex-Undirected-Graph-𝔽 G)
   where
 
   walk-of-length-Undirected-Graph-𝔽 :
@@ -358,7 +366,8 @@ is-vertex-on-walk-cons-walk-Undirected-Graph-𝔽 G =
 
 ```agda
 module _
-  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2) {x : vertex-Undirected-Graph-𝔽 G}
+  {l1 l2 : Level} (G : Undirected-Graph-𝔽 l1 l2)
+  {x : vertex-Undirected-Graph-𝔽 G}
   where
 
   is-vertex-on-first-segment-walk-Undirected-Graph-𝔽 :
@@ -437,7 +446,8 @@ module _
       ( undirected-graph-Undirected-Graph-𝔽 G)
 
   is-constant-walk-Undirected-Graph-𝔽 :
-    {y : vertex-Undirected-Graph-𝔽 G} → walk-Undirected-Graph-𝔽 G x y → UU lzero
+    {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)
 
@@ -525,6 +535,11 @@ module _
   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 = {!!}
+  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/trees/finite-undirected-trees.lagda.md b/src/trees/finite-undirected-trees.lagda.md
index ee8acbaa2f..ab1c20340a 100644
--- a/src/trees/finite-undirected-trees.lagda.md
+++ b/src/trees/finite-undirected-trees.lagda.md
@@ -143,7 +143,8 @@ module _
       ( λ x →
         is-decidable-Π-is-finite
           ( is-finite-vertex-Undirected-Graph-𝔽 G)
-          ( λ y → {!!}))
+          ( λ y →
+            {!!}))
 ```
 
 ### The type of finite undirected trees of cardinality `n` is π-finite

From c589f3a58b72b65c5bb5ebc9479ae2deb0aaf5d9 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 15 Jun 2023 16:31:35 +0200
Subject: [PATCH 08/23] use new convention for is-section and is-retraction

---
 src/foundation/symmetric-operations.lagda.md  | 12 +++++------
 .../walks-finite-undirected-graphs.lagda.md   | 12 +++++------
 .../walks-undirected-graphs.lagda.md          | 20 +++++++++----------
 3 files changed, 22 insertions(+), 22 deletions(-)

diff --git a/src/foundation/symmetric-operations.lagda.md b/src/foundation/symmetric-operations.lagda.md
index eba537b451..995a6cd38e 100644
--- a/src/foundation/symmetric-operations.lagda.md
+++ b/src/foundation/symmetric-operations.lagda.md
@@ -268,10 +268,10 @@ module _
   map-inv-compute-symmetric-operation-Set (f , H) =
     symmetric-operation-is-commutative B f H
 
-  issec-map-inv-compute-symmetric-operation-Set :
+  is-section-map-inv-compute-symmetric-operation-Set :
     ( map-compute-symmetric-operation-Set ∘
       map-inv-compute-symmetric-operation-Set) ~ id
-  issec-map-inv-compute-symmetric-operation-Set (f , H) =
+  is-section-map-inv-compute-symmetric-operation-Set (f , H) =
     eq-type-subtype
       ( is-commutative-Prop B)
       ( eq-htpy
@@ -280,10 +280,10 @@ module _
             ( λ y →
               compute-symmetric-operation-is-commutative B f H x y)))
 
-  isretr-map-inv-compute-symmetric-operation-Set :
+  is-retraction-map-inv-compute-symmetric-operation-Set :
     ( map-inv-compute-symmetric-operation-Set ∘
       map-compute-symmetric-operation-Set) ~ id
-  isretr-map-inv-compute-symmetric-operation-Set g =
+  is-retraction-map-inv-compute-symmetric-operation-Set g =
     eq-htpy-symmetric-operation-Set A B
       ( map-inv-compute-symmetric-operation-Set
         ( map-compute-symmetric-operation-Set g))
@@ -297,8 +297,8 @@ module _
   is-equiv-map-compute-symmetric-operation-Set =
     is-equiv-has-inverse
       map-inv-compute-symmetric-operation-Set
-      issec-map-inv-compute-symmetric-operation-Set
-      isretr-map-inv-compute-symmetric-operation-Set
+      is-section-map-inv-compute-symmetric-operation-Set
+      is-retraction-map-inv-compute-symmetric-operation-Set
 
   compute-symmetric-operation-Set :
     symmetric-operation A (type-Set B) ≃ Σ (A → A → type-Set B) is-commutative
diff --git a/src/graph-theory/walks-finite-undirected-graphs.lagda.md b/src/graph-theory/walks-finite-undirected-graphs.lagda.md
index 2208223259..0d6b458038 100644
--- a/src/graph-theory/walks-finite-undirected-graphs.lagda.md
+++ b/src/graph-theory/walks-finite-undirected-graphs.lagda.md
@@ -186,21 +186,21 @@ module _
       ( undirected-graph-Undirected-Graph-𝔽 G)
       ( x)
 
-  issec-map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 :
+  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
-  issec-map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 =
-    issec-map-inv-compute-total-walk-of-length-Undirected-Graph
+  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)
 
-  isretr-map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 :
+  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
-  isretr-map-inv-compute-total-walk-of-length-Undirected-Graph-𝔽 =
-    isretr-map-inv-compute-total-walk-of-length-Undirected-Graph
+  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)
 
diff --git a/src/graph-theory/walks-undirected-graphs.lagda.md b/src/graph-theory/walks-undirected-graphs.lagda.md
index db9ebe7336..5f1e7f15bb 100644
--- a/src/graph-theory/walks-undirected-graphs.lagda.md
+++ b/src/graph-theory/walks-undirected-graphs.lagda.md
@@ -209,14 +209,14 @@ module _
         ( element-unordered-pair p _)
         ( n , w))
 
-  issec-map-inv-compute-total-walk-of-length-Undirected-Graph :
+  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
-  issec-map-inv-compute-total-walk-of-length-Undirected-Graph y
+  is-section-map-inv-compute-total-walk-of-length-Undirected-Graph y
     ( .0 , refl-walk-of-length-Undirected-Graph) =
     refl
-  issec-map-inv-compute-total-walk-of-length-Undirected-Graph
+  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
@@ -225,23 +225,23 @@ module _
           walk-of-length-Undirected-Graph n (other-element-unordered-pair p _))
         ( succ-ℕ)
         ( λ n → cons-walk-of-length-Undirected-Graph n p e))
-      ( issec-map-inv-compute-total-walk-of-length-Undirected-Graph
+      ( is-section-map-inv-compute-total-walk-of-length-Undirected-Graph
         ( element-unordered-pair p _)
         ( n , w))
 
-  isretr-map-inv-compute-total-walk-of-length-Undirected-Graph :
+  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
-  isretr-map-inv-compute-total-walk-of-length-Undirected-Graph y
+  is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph y
     refl-walk-Undirected-Graph =
     refl
-  isretr-map-inv-compute-total-walk-of-length-Undirected-Graph
+  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)
-      ( isretr-map-inv-compute-total-walk-of-length-Undirected-Graph
+      ( is-retraction-map-inv-compute-total-walk-of-length-Undirected-Graph
         ( element-unordered-pair p _)
         ( w))
 
@@ -251,8 +251,8 @@ module _
   is-equiv-map-compute-total-walk-of-length-Undirected-Graph y =
     is-equiv-has-inverse
       ( map-inv-compute-total-walk-of-length-Undirected-Graph y)
-      ( issec-map-inv-compute-total-walk-of-length-Undirected-Graph y)
-      ( isretr-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) →

From 825b540385900d3544e41ad5293277fe701c8296 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sat, 17 Jun 2023 00:55:59 +0200
Subject: [PATCH 09/23] refactoring

---
 ...rtier-delooping-sign-homomorphism.lagda.md |  19 +-
 .../delooping-sign-homomorphism.lagda.md      |  44 +-
 ...mpson-delooping-sign-homomorphism.lagda.md |  22 +-
 src/foundation-core.lagda.md                  |   1 -
 .../equivalence-induction.lagda.md            |  91 ----
 src/foundation.lagda.md                       |   3 +-
 ...ion-on-equivalences-type-families.lagda.md | 169 ++++++
 src/foundation/equivalence-induction.lagda.md | 246 ++++++++-
 .../symmetric-binary-relations.lagda.md       |  59 +++
 ...univalence-action-on-equivalences.lagda.md | 138 -----
 .../complete-bipartite-graphs.lagda.md        |   2 +-
 .../complete-multipartite-graphs.lagda.md     |   2 +-
 .../complete-undirected-graphs.lagda.md       |   2 +-
 src/graph-theory/undirected-graphs.lagda.md   |  32 +-
 .../walks-directed-graphs.lagda.md            | 494 +++++++++---------
 .../walks-finite-undirected-graphs.lagda.md   |   3 +-
 src/organic-chemistry/ethane.lagda.md         |   2 +-
 src/organic-chemistry/hydrocarbons.lagda.md   |   2 +-
 src/trees/finite-undirected-trees.lagda.md    |   2 +
 .../cyclic-types.lagda.md                     |   2 +
 .../decidable-equivalence-relations.lagda.md  |   2 +-
 .../morphisms-cyclic-types.lagda.md           |   4 +-
 .../reduced-1-bordism-category.lagda.md       |   2 +
 23 files changed, 795 insertions(+), 548 deletions(-)
 delete mode 100644 src/foundation-core/equivalence-induction.lagda.md
 create mode 100644 src/foundation/action-on-equivalences-type-families.lagda.md
 create mode 100644 src/foundation/symmetric-binary-relations.lagda.md
 delete mode 100644 src/foundation/univalence-action-on-equivalences.lagda.md

diff --git a/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md
index 818c2b275a..b3913ddba3 100644
--- a/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md
+++ b/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md
@@ -17,6 +17,7 @@ open import finite-group-theory.finite-type-groups
 open import finite-group-theory.sign-homomorphism
 open import finite-group-theory.transpositions
 
+open import foundation.action-on-equivalences-type-families
 open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
@@ -28,8 +29,8 @@ open import foundation.negation
 open import foundation.propositional-truncations
 open import foundation.raising-universe-levels
 open import foundation.transport
+open import foundation.type-theoretic-principle-of-choice
 open import foundation.unit-type
-open import foundation.univalence-action-on-equivalences
 open import foundation.universe-levels
 
 open import group-theory.concrete-groups
@@ -69,7 +70,7 @@ module _
         ( star)
         ( transposition Y))
       ( map-equiv
-        ( univalent-action-equiv
+        ( action-on-equivalences-family-of-types-subuniverse
           ( mere-equiv-Prop (Fin (n +ℕ 2)))
           ( orientation-Complete-Undirected-Graph (n +ℕ 2))
           ( raise l (Fin (n +ℕ 2)) ,
@@ -110,17 +111,19 @@ module _
           preserves-id-equiv-orientation-complete-undirected-graph-equiv
             ( n +ℕ 2)}
         { y =
-          ( univalent-action-equiv
+          ( action-on-equivalences-family-of-types-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( orientation-Complete-Undirected-Graph (n +ℕ 2))) ,
-          ( preserves-id-equiv-univalent-action-equiv
+          ( compute-id-equiv-action-on-equivalences-family-of-types-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( orientation-Complete-Undirected-Graph (n +ℕ 2)))}
         ( eq-is-contr
-          ( is-contr-preserves-id-action-equiv
-            ( mere-equiv-Prop (Fin (n +ℕ 2)))
-            ( orientation-Complete-Undirected-Graph (n +ℕ 2))
-            ( is-set-orientation-Complete-Undirected-Graph (n +ℕ 2)))))
+          ( is-contr-equiv' _
+            ( distributive-Π-Σ)
+            ( is-contr-Π
+              ( unique-action-on-equivalences-family-of-types-subuniverse
+                  ( mere-equiv-Prop (Fin (n +ℕ 2)))
+                  ( orientation-Complete-Undirected-Graph (n +ℕ 2)))))))
       ( not-even-difference-orientation-aut-transposition-count
         (n +ℕ 2 , (compute-raise l (Fin (n +ℕ 2)))) (star))
 
diff --git a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
index d802a304d7..e7c587e78c 100644
--- a/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
+++ b/src/finite-group-theory/delooping-sign-homomorphism.lagda.md
@@ -18,7 +18,9 @@ open import finite-group-theory.permutations
 open import finite-group-theory.sign-homomorphism
 open import finite-group-theory.transpositions
 
+open import foundation.action-on-equivalences-type-families
 open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
 open import foundation.commuting-squares-of-maps
 open import foundation.contractible-types
 open import foundation.coproduct-types
@@ -30,6 +32,7 @@ open import foundation.empty-types
 open import foundation.equality-dependent-pair-types
 open import foundation.equivalence-classes
 open import foundation.equivalence-extensionality
+open import foundation.equivalence-induction
 open import foundation.equivalence-relations
 open import foundation.equivalences
 open import foundation.function-extensionality
@@ -52,7 +55,6 @@ open import foundation.truncated-types
 open import foundation.uniqueness-set-quotients
 open import foundation.unit-type
 open import foundation.univalence
-open import foundation.univalence-action-on-equivalences
 open import foundation.universal-property-set-quotients
 open import foundation.universe-levels
 
@@ -120,7 +122,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-Eq-Rel
       ( R
@@ -129,7 +132,7 @@ module _
           unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))
       ( quotient-aut-succ-succ-Fin n (transposition Y))
       ( map-equiv
-        ( univalent-action-equiv
+        ( action-on-equivalences-family-of-types-subuniverse
           ( mere-equiv-Prop (Fin (n +ℕ 2)))
           ( D (n +ℕ 2))
           ( raise l1 (Fin (n +ℕ 2)) ,
@@ -165,13 +168,17 @@ module _
       (n : ℕ) (X X' : UU-Fin l1 n) →
       type-UU-Fin n X ≃ type-UU-Fin n X' → D n X ≃ D n X'
     invertible-action-D-equiv n =
-      univalent-action-equiv (mere-equiv-Prop (Fin n)) (D n)
+      action-on-equivalences-family-of-types-subuniverse
+        ( mere-equiv-Prop (Fin n))
+        ( D n)
 
     preserves-id-equiv-invertible-action-D-equiv :
       (n : ℕ) (X : UU-Fin l1 n) →
       Id (invertible-action-D-equiv n X X id-equiv) id-equiv
     preserves-id-equiv-invertible-action-D-equiv n =
-      preserves-id-equiv-univalent-action-equiv (mere-equiv-Prop (Fin n)) (D n)
+      compute-id-equiv-action-on-equivalences-family-of-types-subuniverse
+        ( mere-equiv-Prop (Fin n))
+        ( D n)
 
     preserves-R-invertible-action-D-equiv :
       ( n : ℕ) →
@@ -183,14 +190,29 @@ module _
           ( R n X')
           ( map-equiv (invertible-action-D-equiv n X X' e) a)
           ( map-equiv (invertible-action-D-equiv n X X' e) a'))
-    preserves-R-invertible-action-D-equiv n X X' =
-      Ind-univalent-action-equiv (mere-equiv-Prop (Fin n)) (D n) X
+    preserves-R-invertible-action-D-equiv n X =
+      ind-equiv-subuniverse
+        ( mere-equiv-Prop (Fin n))
+        ( X)
         ( λ Y f →
           ( a a' : D n X) →
           ( sim-Eq-Rel (R n X) a a' ↔
-            sim-Eq-Rel (R n Y) (map-equiv f a) (map-equiv f a')))
-        ( λ a a' → id , id)
-        ( X')
+            sim-Eq-Rel
+              ( R n Y)
+              ( map-equiv (invertible-action-D-equiv n X Y f) a)
+              ( map-equiv (invertible-action-D-equiv n X Y f) a')))
+        ( λ a a' →
+          ( iff-equiv
+            ( equiv-binary-tr
+              ( sim-Eq-Rel (R n X))
+              ( inv
+                ( ap
+                  ( λ g → map-equiv g a)
+                  ( preserves-id-equiv-invertible-action-D-equiv n X)))
+              ( inv
+                ( ap
+                  ( λ g → map-equiv g a')
+                  ( preserves-id-equiv-invertible-action-D-equiv n X))))))
 
     raise-UU-Fin-Fin : (n : ℕ) → UU-Fin l1 n
     pr1 (raise-UU-Fin-Fin n) = raise l1 (Fin n)
@@ -1488,7 +1510,7 @@ module _
             unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))) →
     ¬ ( x ＝
         ( map-equiv
-          ( univalent-action-equiv
+          ( action-on-equivalences-family-of-types-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( type-UU-Fin 2 ∘ Q (n +ℕ 2))
             ( raise l1 (Fin (n +ℕ 2)) ,
diff --git a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md
index ac21a80e6a..11d543cb6e 100644
--- a/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md
+++ b/src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md
@@ -21,6 +21,7 @@ open import finite-group-theory.permutations
 open import finite-group-theory.sign-homomorphism
 open import finite-group-theory.transpositions
 
+open import foundation.action-on-equivalences-type-families
 open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.coproduct-types
@@ -42,8 +43,8 @@ open import foundation.propositional-truncations
 open import foundation.raising-universe-levels
 open import foundation.sets
 open import foundation.transport
+open import foundation.type-theoretic-principle-of-choice
 open import foundation.unit-type
-open import foundation.univalence-action-on-equivalences
 open import foundation.universe-levels
 
 open import group-theory.concrete-groups
@@ -681,7 +682,7 @@ module _
           unit-trunc-Prop (compute-raise-Fin l (n +ℕ 2))))
       ( sign-comp-aut-succ-succ-Fin n (transposition Y))
       ( map-equiv
-        ( univalent-action-equiv
+        ( action-on-equivalences-family-of-types-subuniverse
           ( mere-equiv-Prop (Fin (n +ℕ 2)))
           ( λ X → Fin (n +ℕ 2) ≃ pr1 X)
           ( raise l (Fin (n +ℕ 2)) ,
@@ -714,20 +715,19 @@ module _
           simpson-comp-equiv (n +ℕ 2) ,
           preserves-id-equiv-simpson-comp-equiv (n +ℕ 2)}
         { y =
-          ( univalent-action-equiv
+          ( action-on-equivalences-family-of-types-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X) ,
-            ( preserves-id-equiv-univalent-action-equiv
+            ( compute-id-equiv-action-on-equivalences-family-of-types-subuniverse
               ( mere-equiv-Prop (Fin (n +ℕ 2)))
               ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X)))}
         ( eq-is-contr
-          ( is-contr-preserves-id-action-equiv
-            ( mere-equiv-Prop (Fin (n +ℕ 2)))
-            ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X)
-            ( λ X →
-              is-set-equiv-is-set
-                ( is-set-Fin (n +ℕ 2))
-                ( is-set-type-UU-Fin (n +ℕ 2) X)))))
+          ( is-contr-equiv' _
+            ( distributive-Π-Σ)
+            ( is-contr-Π
+              ( unique-action-on-equivalences-family-of-types-subuniverse
+                ( mere-equiv-Prop (Fin (n +ℕ 2)))
+                ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X))))))
       ( not-sign-comp-transposition-count
         (n +ℕ 2 , (compute-raise l (Fin (n +ℕ 2)))) (star))
 
diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md
index ad4d0da68a..36ce8db861 100644
--- a/src/foundation-core.lagda.md
+++ b/src/foundation-core.lagda.md
@@ -24,7 +24,6 @@ open import foundation-core.embeddings public
 open import foundation-core.empty-types public
 open import foundation-core.endomorphisms public
 open import foundation-core.equality-dependent-pair-types public
-open import foundation-core.equivalence-induction public
 open import foundation-core.equivalence-relations public
 open import foundation-core.equivalences public
 open import foundation-core.fibers-of-maps public
diff --git a/src/foundation-core/equivalence-induction.lagda.md b/src/foundation-core/equivalence-induction.lagda.md
deleted file mode 100644
index ce2e4826d6..0000000000
--- a/src/foundation-core/equivalence-induction.lagda.md
+++ /dev/null
@@ -1,91 +0,0 @@
-# Equivalence induction
-
-```agda
-module foundation-core.equivalence-induction where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.dependent-pair-types
-open import foundation.universe-levels
-
-open import foundation-core.contractible-types
-open import foundation-core.equivalences
-open import foundation-core.function-types
-open import foundation-core.homotopies
-open import foundation-core.identity-types
-open import foundation-core.sections
-open import foundation-core.singleton-induction
-```
-
-</details>
-
-## Idea
-
-Equivalence induction is a condition equivalent to the univalence axiom
-
-## Properties
-
-```agda
-module _
-  {l1 : Level} {A : UU l1}
-  where
-
-  ev-id :
-    { l : Level} (P : (B : UU l1) → (A ≃ B) → UU l) →
-    ( (B : UU l1) (e : A ≃ B) → P B e) → P A id-equiv
-  ev-id P f = f A id-equiv
-
-  IND-EQUIV :
-    {l : Level} (P : (B : UU l1) (e : A ≃ B) → UU l) → UU (lsuc l1 ⊔ l)
-  IND-EQUIV P = section (ev-id P)
-
-  triangle-ev-id :
-    { l : Level}
-    ( P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) →
-    ( ev-point (pair A id-equiv) {P}) ~
-    ( ( ev-id (λ X e → P (pair X e))) ∘
-      ( ev-pair {A = UU l1} {B = λ X → A ≃ X} {C = P}))
-  triangle-ev-id P f = refl
-```
-
-### Contractibility of the total space of equivalences implies equivalence induction
-
-```agda
-  abstract
-    IND-EQUIV-is-contr-total-equiv :
-      is-contr (Σ (UU l1) (λ X → A ≃ X)) →
-      {l : Level} →
-      (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) → IND-EQUIV (λ B e → P (pair B e))
-    IND-EQUIV-is-contr-total-equiv c P =
-      section-left-factor
-        ( ev-id (λ X e → P (pair X e)))
-        ( ev-pair)
-        ( is-singleton-is-contr
-          ( pair A id-equiv)
-          ( pair
-            ( pair A id-equiv)
-            ( λ t → ( inv (contraction c (pair A id-equiv))) ∙
-                    ( contraction c t)))
-          ( P))
-```
-
-### Equivalence induction implies contractibility of the total space of equivalences
-
-```agda
-  abstract
-    is-contr-total-equiv-IND-EQUIV :
-      ( {l : Level} (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) →
-        IND-EQUIV (λ B e → P (pair B e))) →
-      is-contr (Σ (UU l1) (λ X → A ≃ X))
-    is-contr-total-equiv-IND-EQUIV ind =
-      is-contr-is-singleton
-        ( Σ (UU l1) (λ X → A ≃ X))
-        ( pair A id-equiv)
-        ( λ P → section-comp
-          ( ev-id (λ X e → P (pair X e)))
-          ( ev-pair {A = UU l1} {B = λ X → A ≃ X} {C = P})
-          ( pair ind-Σ refl-htpy)
-          ( ind P))
-```
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 9b7118763f..54121fc69c 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -10,6 +10,7 @@ open import foundation.0-images-of-maps public
 open import foundation.0-maps public
 open import foundation.1-types public
 open import foundation.2-types public
+open import foundation.action-on-equivalences-type-families public
 open import foundation.action-on-identifications-binary-functions public
 open import foundation.action-on-identifications-dependent-functions public
 open import foundation.action-on-identifications-functions public
@@ -246,6 +247,7 @@ open import foundation.subtype-identity-principle public
 open import foundation.subtypes public
 open import foundation.subuniverses public
 open import foundation.surjective-maps public
+open import foundation.symmetric-binary-relations public
 open import foundation.symmetric-difference public
 open import foundation.symmetric-identity-types public
 open import foundation.symmetric-operations public
@@ -281,7 +283,6 @@ open import foundation.uniqueness-truncation public
 open import foundation.unit-type public
 open import foundation.unital-binary-operations public
 open import foundation.univalence public
-open import foundation.univalence-action-on-equivalences public
 open import foundation.univalence-implies-function-extensionality public
 open import foundation.univalent-type-families public
 open import foundation.universal-property-booleans public
diff --git a/src/foundation/action-on-equivalences-type-families.lagda.md b/src/foundation/action-on-equivalences-type-families.lagda.md
new file mode 100644
index 0000000000..07ca2b5a04
--- /dev/null
+++ b/src/foundation/action-on-equivalences-type-families.lagda.md
@@ -0,0 +1,169 @@
+# Action on equivalences of type families
+
+```agda
+module foundation.action-on-equivalences-type-families where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.equivalence-induction
+open import foundation.fibers-of-maps
+open import foundation.function-extensionality
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.subuniverses
+open import foundation.transport
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import foundation-core.contractible-types
+open import foundation-core.equality-dependent-pair-types
+open import foundation-core.equivalences
+open import foundation-core.injective-maps
+open import foundation-core.propositions
+open import foundation-core.subtypes
+```
+
+</details>
+
+## Ideas
+
+Given a [subuniverse](foundation.subuniverses.md) `P`, any family of types `B`
+indexed by types of `P` has an **action on equivalences**
+
+```text
+  (A ≃ B) → P A ≃ P B
+```
+
+obtained by [equivalence induction](foundation.equivalence-induction.md). The
+acion on equivalences of a type family `B` on a subuniverse `P` of `𝒰` is such
+that `B id-equiv ＝ id-equiv`, and fits in a
+[commuting square](foundation.commuting-squares-of-maps.md)
+
+```text
+                   ap B
+        (X ＝ Y) --------> (B X ＝ B Y)
+           |                    |
+  equiv-eq |                    | equiv-eq
+           V                    V
+        (X ≃ Y) ---------> (B X ≃ B Y).
+                     B
+```
+
+## Definitions
+
+### The action on equivalences of a family of types over a subuniverse
+
+```agda
+module _
+  { l1 l2 l3 : Level}
+  ( P : subuniverse l1 l2) (B : type-subuniverse P → UU l3)
+  where
+
+  unique-action-on-equivalences-family-of-types-subuniverse :
+    (X : type-subuniverse P) →
+    is-contr (fib (ev-id-equiv-subuniverse P X {λ Y e → B X ≃ B Y}) id-equiv)
+  unique-action-on-equivalences-family-of-types-subuniverse X =
+    is-contr-map-ev-id-equiv-subuniverse P X (λ Y e → B X ≃ B Y) id-equiv
+
+  action-on-equivalences-family-of-types-subuniverse :
+    (X Y : type-subuniverse P) → pr1 X ≃ pr1 Y → B X ≃ B Y
+  action-on-equivalences-family-of-types-subuniverse X =
+    pr1 (center (unique-action-on-equivalences-family-of-types-subuniverse X))
+
+  compute-id-equiv-action-on-equivalences-family-of-types-subuniverse :
+    (X : type-subuniverse P) →
+    action-on-equivalences-family-of-types-subuniverse X X id-equiv ＝ id-equiv
+  compute-id-equiv-action-on-equivalences-family-of-types-subuniverse X =
+    pr2 (center (unique-action-on-equivalences-family-of-types-subuniverse X))
+```
+
+### The action on equivalences of a family of types over a universe
+
+```agda
+module _
+  {l1 l2 : Level} (B : UU l1 → UU l2)
+  where
+
+  unique-action-on-equivalences-family-of-types-universe :
+    {X : UU l1} →
+    is-contr (fib (ev-id-equiv (λ Y e → B X ≃ B Y)) id-equiv)
+  unique-action-on-equivalences-family-of-types-universe =
+    is-contr-map-ev-id-equiv (λ Y e → B _ ≃ B Y) id-equiv
+
+  action-on-equivalences-family-of-types-universe :
+    {X Y : UU l1} → (X ≃ Y) → B X ≃ B Y
+  action-on-equivalences-family-of-types-universe {X} {Y} =
+    pr1 (center (unique-action-on-equivalences-family-of-types-universe {X})) Y
+
+  compute-id-equiv-action-on-equivalences-family-of-types-universe :
+    {X : UU l1} →
+    action-on-equivalences-family-of-types-universe {X} {X} id-equiv ＝ id-equiv
+  compute-id-equiv-action-on-equivalences-family-of-types-universe {X} =
+    pr2 (center (unique-action-on-equivalences-family-of-types-universe {X}))
+```
+
+## Properties
+
+### The action on equivalences of a family of types over a subuniverse fits in a commuting square with `equiv-eq`
+
+We claim that the square
+
+```text
+                   ap B
+        (X ＝ Y) --------> (B X ＝ B Y)
+           |                    |
+  equiv-eq |                    | equiv-eq
+           V                    V
+        (X ≃ Y) ---------> (B X ≃ B Y).
+                     B
+```
+
+commutes for any two types `X Y : type-subuniverse P` and any family of types
+`B` over the subuniverse `P`.
+
+```agda
+coherence-square-action-on-equivalences-family-of-types-subuniverse :
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (B : type-subuniverse P → UU l3) →
+  (X Y : type-subuniverse P) →
+  coherence-square-maps
+    ( ap B {X} {Y})
+    ( equiv-eq-subuniverse P X Y)
+    ( equiv-eq)
+    ( action-on-equivalences-family-of-types-subuniverse P B X Y)
+coherence-square-action-on-equivalences-family-of-types-subuniverse
+  P B X .X refl =
+  compute-id-equiv-action-on-equivalences-family-of-types-subuniverse P B X
+```
+
+### The action on equivalences of a family of types over a universe fits in a commuting square with `equiv-eq`
+
+We claim that the square
+
+```text
+                   ap B
+        (X ＝ Y) --------> (B X ＝ B Y)
+           |                    |
+  equiv-eq |                    | equiv-eq
+           V                    V
+        (X ≃ Y) ---------> (B X ≃ B Y).
+                     B
+```
+
+commutes for any two types `X Y : 𝒰` and any type family `B` over `𝒰`.
+
+```agda
+coherence-square-action-on-equivalences-family-of-types-universe :
+  {l1 l2 : Level} (B : UU l1 → UU l2) (X Y : UU l1) →
+  coherence-square-maps
+    ( ap B {X} {Y})
+    ( equiv-eq)
+    ( equiv-eq)
+    ( action-on-equivalences-family-of-types-universe B)
+coherence-square-action-on-equivalences-family-of-types-universe B X .X refl =
+  compute-id-equiv-action-on-equivalences-family-of-types-universe B
+```
diff --git a/src/foundation/equivalence-induction.lagda.md b/src/foundation/equivalence-induction.lagda.md
index 5fe4716a37..1682243778 100644
--- a/src/foundation/equivalence-induction.lagda.md
+++ b/src/foundation/equivalence-induction.lagda.md
@@ -2,53 +2,257 @@
 
 ```agda
 module foundation.equivalence-induction where
-
-open import foundation-core.equivalence-induction public
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.contractible-maps
+open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.identity-systems
+open import foundation.identity-types
+open import foundation.subuniverses
 open import foundation.univalence
+open import foundation.universal-property-dependent-pair-types
 open import foundation.universe-levels
 
+open import foundation-core.commuting-triangles-of-maps
 open import foundation-core.equivalences
 open import foundation-core.function-types
+open import foundation-core.homotopies
 open import foundation-core.sections
+open import foundation-core.singleton-induction
 ```
 
 </details>
 
 ## Idea
 
-Equivalence induction is a condition equivalent to the univalence axiom
+**Equivalence induction** is the principle asserting that for any type family
+
+```text
+  P : (B : 𝒰) (e : A ≃ B) → 𝒰
+```
+
+of types indexed by all [equivalences](foundation.equivalences.md) with domain
+`A`, there is a [section](foundation.sections.md) of the evaluation map
+
+```text
+  ((B : 𝒰) (e : A ≃ B) → P B e) → P A id-equiv.
+```
+
+The principle of equivalence induction is equivalent to the
+[univalence axiom](foundation.univalence.md).
 
-## Theorem
+By equivalence induction, it follows that any type family `P : 𝒰 → 𝒱` on the
+universe has an
+[action on equivalences](foundation.action-on-equivalences-type-families.md)
+
+```text
+  (A ≃ B) → P A ≃ P B.
+```
+
+## Statement
 
 ```agda
-abstract
-  Ind-equiv :
-    {l1 l2 : Level} (A : UU l1) (P : (B : UU l1) (e : A ≃ B) → UU l2) →
-    section (ev-id P)
-  Ind-equiv A P =
-    IND-EQUIV-is-contr-total-equiv
-    ( is-contr-total-equiv A)
-    ( λ t → P (pr1 t) (pr2 t))
+module _
+  {l1 : Level} {A : UU l1}
+  where
+
+  ev-id-equiv :
+    {l : Level} (P : (B : UU l1) → (A ≃ B) → UU l) →
+    ((B : UU l1) (e : A ≃ B) → P B e) → P A id-equiv
+  ev-id-equiv P f = f A id-equiv
+
+  IND-EQUIV :
+    {l : Level} (P : (B : UU l1) (e : A ≃ B) → UU l) → UU (lsuc l1 ⊔ l)
+  IND-EQUIV P = section (ev-id-equiv P)
+
+  triangle-ev-id-equiv :
+    {l : Level}
+    (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) →
+    coherence-triangle-maps
+      ( ev-point (pair A id-equiv) {P})
+      ( ev-id-equiv (λ X e → P (pair X e)))
+      ( ev-pair {A = UU l1} {B = λ X → A ≃ X} {C = P})
+  triangle-ev-id-equiv P f = refl
+```
+
+## Properties
+
+### Equivalence induction is equivalent to the contractibility of the total space of equivalences
+
+#### Contractibility of the total space of equivalences implies equivalence induction
+
+```agda
+module _
+  {l1 : Level} {A : UU l1}
+  where
+
+  abstract
+    IND-EQUIV-is-contr-total-equiv :
+      is-contr (Σ (UU l1) (λ X → A ≃ X)) →
+      {l : Level} →
+      (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) → IND-EQUIV (λ B e → P (pair B e))
+    IND-EQUIV-is-contr-total-equiv c P =
+      section-left-factor
+        ( ev-id-equiv (λ X e → P (pair X e)))
+        ( ev-pair)
+        ( is-singleton-is-contr
+          ( pair A id-equiv)
+          ( pair
+            ( pair A id-equiv)
+            ( λ t → ( inv (contraction c (pair A id-equiv))) ∙
+                    ( contraction c t)))
+          ( P))
+```
+
+#### Equivalence induction implies contractibility of the total space of equivalences
+
+```agda
+module _
+  {l1 : Level} {A : UU l1}
+  where
+
+  abstract
+    is-contr-total-equiv-IND-EQUIV :
+      ( {l : Level} (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) →
+        IND-EQUIV (λ B e → P (pair B e))) →
+      is-contr (Σ (UU l1) (λ X → A ≃ X))
+    is-contr-total-equiv-IND-EQUIV ind =
+      is-contr-is-singleton
+        ( Σ (UU l1) (λ X → A ≃ X))
+        ( pair A id-equiv)
+        ( λ P → section-comp
+          ( ev-id-equiv (λ X e → P (pair X e)))
+          ( ev-pair {A = UU l1} {B = λ X → A ≃ X} {C = P})
+          ( pair ind-Σ refl-htpy)
+          ( ind P))
+```
+
+### Equivalence induction in a universe
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (P : (B : UU l1) (e : A ≃ B) → UU l2)
+  where
+
+  abstract
+    Ind-equiv : section (ev-id-equiv P)
+    Ind-equiv =
+      IND-EQUIV-is-contr-total-equiv
+      ( is-contr-total-equiv _)
+      ( λ t → P (pr1 t) (pr2 t))
+
+  ind-equiv :
+    P A id-equiv → {B : UU l1} (e : A ≃ B) → P B e
+  ind-equiv p {B} = pr1 Ind-equiv p B
+
+  compute-ind-equiv :
+    (u : P A id-equiv) → ind-equiv u id-equiv ＝ u
+  compute-ind-equiv = pr2 Ind-equiv
+```
+
+### Equivalence induction in a subuniverse
+
+```agda
+module _
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (A : type-subuniverse P)
+  where
+
+  ev-id-equiv-subuniverse :
+    {F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3} →
+    ((B : type-subuniverse P) (e : equiv-subuniverse P A B) → F B e) →
+    F A id-equiv
+  ev-id-equiv-subuniverse f = f A id-equiv
+
+  triangle-ev-id-equiv-subuniverse :
+    (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) →
+    coherence-triangle-maps
+      ( ev-point (A , id-equiv))
+      ( ev-id-equiv-subuniverse {F})
+      ( ev-pair)
+  triangle-ev-id-equiv-subuniverse F E = refl
 
-ind-equiv :
-  {l1 l2 : Level} (A : UU l1) (P : (B : UU l1) (e : A ≃ B) → UU l2) →
-  P A id-equiv → {B : UU l1} (e : A ≃ B) → P B e
-ind-equiv A P p {B} = pr1 (Ind-equiv A P) p B
+  abstract
+    Ind-equiv-subuniverse :
+      (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) →
+      section (ev-id-equiv-subuniverse {F})
+    Ind-equiv-subuniverse =
+      Ind-identity-system A id-equiv (is-contr-total-equiv-subuniverse P A)
+
+  ind-equiv-subuniverse :
+    (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) →
+    F A id-equiv → (B : type-subuniverse P) (e : equiv-subuniverse P A B) →
+    F B e
+  ind-equiv-subuniverse F = pr1 (Ind-equiv-subuniverse F)
+
+  compute-ind-equiv-subuniverse :
+    (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) →
+    (u : F A id-equiv) →
+    ind-equiv-subuniverse F u A id-equiv ＝ u
+  compute-ind-equiv-subuniverse F = pr2 (Ind-equiv-subuniverse F)
 ```
 
-## Corollaries
+### The evaluation map `ev-id-equiv` is an equivalence
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (P : (B : UU l1) (e : A ≃ B) → UU l2)
+  where
+
+  is-equiv-ev-id-equiv : is-equiv (ev-id-equiv P)
+  is-equiv-ev-id-equiv =
+    is-equiv-left-factor-htpy
+      ( ev-point (A , id-equiv))
+      ( ev-id-equiv P)
+      ( ev-pair)
+      ( triangle-ev-id-equiv (λ u → P (pr1 u) (pr2 u)))
+      ( dependent-universal-property-contr-is-contr
+        ( A , id-equiv)
+        ( is-contr-total-equiv A)
+        ( λ u → P (pr1 u) (pr2 u)))
+      ( is-equiv-ev-pair)
+
+  is-contr-map-ev-id-equiv : is-contr-map (ev-id-equiv P)
+  is-contr-map-ev-id-equiv = is-contr-map-is-equiv is-equiv-ev-id-equiv
+```
+
+### The evaluation map `ev-id-equiv-subuniverse` is an equivalence
+
+```agda
+module _
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (X : type-subuniverse P)
+  (F : (Y : type-subuniverse P) (e : equiv-subuniverse P X Y) → UU l3)
+  where
+
+  is-equiv-ev-id-equiv-subuniverse :
+    is-equiv (ev-id-equiv-subuniverse P X {F})
+  is-equiv-ev-id-equiv-subuniverse =
+    is-equiv-left-factor-htpy
+      ( ev-point (X , id-equiv))
+      ( ev-id-equiv-subuniverse P X)
+      ( ev-pair)
+      ( triangle-ev-id-equiv-subuniverse P X F)
+      ( dependent-universal-property-contr-is-contr
+        ( X , id-equiv)
+        ( is-contr-total-equiv-subuniverse P X)
+        ( λ E → F (pr1 E) (pr2 E)))
+      ( is-equiv-ev-pair)
+
+  is-contr-map-ev-id-equiv-subuniverse :
+    is-contr-map (ev-id-equiv-subuniverse P X {F})
+  is-contr-map-ev-id-equiv-subuniverse =
+    is-contr-map-is-equiv is-equiv-ev-id-equiv-subuniverse
+```
 
 ### Equivalence induction implies that postcomposing by an equivalence is an equivalence
 
-Of course we already know this fact from function extensionality, but we prove
-it again from equivalence induction so that we can prove that univalence implies
-function extensionality.
+Of course we already know that this fact follows from
+[function extensionality](foundation.function-extensionality.md). However, we
+prove it again from equivalence induction so that we can prove that
+[univalence implies function extensionality](foundation.univalence-implies-function-extensionality.md).
 
 ```agda
 abstract
@@ -56,5 +260,5 @@ abstract
     {l1 l2 : Level} {X Y : UU l1} (A : UU l2) (e : X ≃ Y) →
     is-equiv (postcomp A (map-equiv e))
   is-equiv-postcomp-univalence {X = X} A =
-    ind-equiv X (λ Y e → is-equiv (postcomp A (map-equiv e))) is-equiv-id
+    ind-equiv (λ Y e → is-equiv (postcomp A (map-equiv e))) is-equiv-id
 ```
diff --git a/src/foundation/symmetric-binary-relations.lagda.md b/src/foundation/symmetric-binary-relations.lagda.md
new file mode 100644
index 0000000000..d00278edd7
--- /dev/null
+++ b/src/foundation/symmetric-binary-relations.lagda.md
@@ -0,0 +1,59 @@
+# Symmetric binary relations
+
+```agda
+module foundation.symmetric-binary-relations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-equivalences-type-families
+open import foundation.equivalences
+open import foundation.transport
+open import foundation.universe-levels
+open import foundation.unordered-pairs
+```
+
+</details>
+
+## Idea
+
+A **symmetric binary relation** on a type `A` is a type family `R` over the type
+of [unordered pairs](foundation.unordered-pairs.md) of elements of `A`. Given a
+symmetric binary relation `R` on `A` and an equivalence of unordered pairs
+`p ＝ q`, we have `R p ≃ R q`. In particular, we have
+
+```text
+  R ({x,y}) ≃ R ({y,x})
+```
+
+for any two elements `x y : A`, where `{x,y}` is the _standard unordered pair_
+consisting of `x` and `y`.
+
+## Definitions
+
+### Symmetric binary relations
+
+```agda
+symmetric-binary-relation :
+  {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
+symmetric-binary-relation l2 A = unordered-pair A → UU l2
+```
+
+### Symmetries of symmetric binary relations
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : symmetric-binary-relation l2 A)
+  where
+
+  equiv-tr-symmetric-binary-relation :
+    (p q : unordered-pair A) → Eq-unordered-pair p q → R p ≃ R q
+  equiv-tr-symmetric-binary-relation p q e =
+    equiv-tr R (eq-Eq-unordered-pair' p q e)
+
+  tr-symmetric-binary-relation :
+    (p q : unordered-pair A) → Eq-unordered-pair p q → R p → R q
+  tr-symmetric-binary-relation p q e =
+    map-equiv (equiv-tr-symmetric-binary-relation p q e)
+```
diff --git a/src/foundation/univalence-action-on-equivalences.lagda.md b/src/foundation/univalence-action-on-equivalences.lagda.md
deleted file mode 100644
index c14a375bfd..0000000000
--- a/src/foundation/univalence-action-on-equivalences.lagda.md
+++ /dev/null
@@ -1,138 +0,0 @@
-# Univalent action on equivalences
-
-```agda
-module foundation.univalence-action-on-equivalences where
-```
-
-<details><summary>Imports</summary>
-
-```agda
-open import foundation.action-on-identifications-functions
-open import foundation.dependent-pair-types
-open import foundation.function-extensionality
-open import foundation.identity-types
-open import foundation.sets
-open import foundation.subuniverses
-open import foundation.transport
-open import foundation.univalence
-open import foundation.universe-levels
-
-open import foundation-core.contractible-types
-open import foundation-core.equality-dependent-pair-types
-open import foundation-core.equivalences
-open import foundation-core.injective-maps
-open import foundation-core.propositions
-open import foundation-core.subtypes
-```
-
-</details>
-
-## Ideas
-
-Given a subuniverse `P`, any family of types `B` indexed by types of `P` has an
-action on equivalences obtained by using the univalence axiom.
-
-## Definition
-
-```agda
-module _
-  { l1 l2 l3 : Level}
-  ( P : subuniverse l1 l2) (B : type-subuniverse P → UU l3)
-  where
-
-  univalent-action-equiv :
-    (X Y : type-subuniverse P) → pr1 X ≃ pr1 Y → B X ≃ B Y
-  univalent-action-equiv X Y e = equiv-tr B (eq-equiv-subuniverse P e)
-```
-
-## Properties
-
-```agda
-  preserves-id-equiv-univalent-action-equiv :
-    (X : type-subuniverse P) →
-    univalent-action-equiv X X id-equiv ＝ id-equiv
-  preserves-id-equiv-univalent-action-equiv X =
-    ( ap (equiv-tr B)
-      ( is-injective-map-equiv
-        ( extensionality-subuniverse P X X)
-        ( is-section-map-inv-is-equiv
-          ( is-equiv-equiv-eq-subuniverse P X X)
-          ( id-equiv)))) ∙
-      ( equiv-tr-refl B)
-
-  Ind-univalent-action-path :
-    { l4 : Level}
-    ( X : type-subuniverse P)
-    ( F : (Y : type-subuniverse P) → B X ≃ B Y → UU l4) →
-    F X id-equiv → ( Y : type-subuniverse P) (p : X ＝ Y) →
-    F Y (equiv-tr B p)
-  Ind-univalent-action-path X F p .X refl =
-    tr (F X) (inv (equiv-tr-refl B)) p
-
-  Ind-univalent-action-equiv :
-    { l4 : Level}
-    ( X : type-subuniverse P)
-    ( F : (Y : type-subuniverse P) → B X ≃ B Y → UU l4) →
-    F X id-equiv → (Y : type-subuniverse P) (e : pr1 X ≃ pr1 Y) →
-    F Y (univalent-action-equiv X Y e)
-  Ind-univalent-action-equiv X F p Y e =
-    Ind-univalent-action-path X F p Y (eq-equiv-subuniverse P e)
-
-  is-contr-preserves-id-action-equiv :
-    ( (X : type-subuniverse P) → is-set (B X)) →
-    is-contr
-      ( Σ
-        ( (X Y : type-subuniverse P) → pr1 X ≃ pr1 Y → B X ≃ B Y)
-        ( λ D → (X : type-subuniverse P) → D X X id-equiv ＝ id-equiv))
-  pr1 (pr1 (is-contr-preserves-id-action-equiv H)) = univalent-action-equiv
-  pr2 (pr1 (is-contr-preserves-id-action-equiv H)) =
-    preserves-id-equiv-univalent-action-equiv
-  pr2 (is-contr-preserves-id-action-equiv H) (D , p) =
-    eq-pair-Σ
-      ( eq-htpy (λ X → eq-htpy (λ Y → eq-htpy (λ e →
-        lemma2 univalent-action-equiv D
-          (λ X → preserves-id-equiv-univalent-action-equiv X ∙ inv (p X))
-          X Y e))))
-      ( eq-is-prop
-        ( is-prop-Π
-          ( λ X →
-            is-set-type-Set
-              ( B X ≃ B X , is-set-equiv-is-set (H X) (H X))
-              ( D X X id-equiv)
-              ( id-equiv))))
-    where
-    lemma1 :
-      (f g : (X Y : UU l1) → (pX : is-in-subuniverse P X) →
-        ( pY : is-in-subuniverse P Y) → X ＝ Y →
-        B (X , pX) ≃ B (Y , pY)) →
-      ( (X : UU l1) (pX : is-in-subuniverse P X)
-        (pX' : is-in-subuniverse P X) →
-        f X X pX pX' refl ＝ g X X pX pX' refl) →
-      ( X Y : UU l1) (pX : is-in-subuniverse P X)
-      ( pY : is-in-subuniverse P Y) (p : X ＝ Y) →
-      f X Y pX pY p ＝ g X Y pX pY p
-    lemma1 f g h X .X pX pX' refl = h X pX pX'
-    lemma2 :
-      ( f g : (X Y : type-subuniverse P) → pr1 X ≃ pr1 Y → B X ≃ B Y) →
-      ( (X : type-subuniverse P) → f X X id-equiv ＝ g X X id-equiv) →
-      ( X Y : type-subuniverse P) (e : pr1 X ≃ pr1 Y) →
-      f X Y e ＝ g X Y e
-    lemma2 f g h X Y e =
-      tr
-        ( λ e' → f X Y e' ＝ g X Y e')
-        ( is-section-map-inv-is-equiv (univalence (pr1 X) (pr1 Y)) e)
-        ( lemma1
-          ( λ X Y pX pY p → f (X , pX) (Y , pY) (equiv-eq p))
-          ( λ X Y pX pY p → g (X , pX) (Y , pY) (equiv-eq p))
-          ( λ X pX pX' →
-            tr
-              ( λ p → f (X , pX) (X , p) id-equiv ＝
-                g (X , pX) (X , p) id-equiv)
-              ( eq-is-prop (is-prop-is-in-subtype P X))
-              ( h ( X , pX)))
-          ( pr1 X)
-          ( pr1 Y)
-          ( pr2 X)
-          ( pr2 Y)
-          ( eq-equiv (pr1 X) (pr1 Y) e))
-```
diff --git a/src/graph-theory/complete-bipartite-graphs.lagda.md b/src/graph-theory/complete-bipartite-graphs.lagda.md
index ebb0cdfd4b..bfa04b5f1f 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 bf6a9f671f..ce4cd32139 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 0fa96550c6..7061c52f20 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/undirected-graphs.lagda.md b/src/graph-theory/undirected-graphs.lagda.md
index e2feaad31a..90ac67956c 100644
--- a/src/graph-theory/undirected-graphs.lagda.md
+++ b/src/graph-theory/undirected-graphs.lagda.md
@@ -1,6 +1,8 @@
 # Undirected graphs
 
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module graph-theory.undirected-graphs where
 ```
 
@@ -81,18 +83,26 @@ 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 =
+  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 = {!!}
 ```
 
 ### Transporting edges along equalities of unordered pairs of vertices
diff --git a/src/graph-theory/walks-directed-graphs.lagda.md b/src/graph-theory/walks-directed-graphs.lagda.md
index cb327fdab1..cdfdb4529b 100644
--- a/src/graph-theory/walks-directed-graphs.lagda.md
+++ b/src/graph-theory/walks-directed-graphs.lagda.md
@@ -109,6 +109,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
@@ -225,6 +310,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
index 0d6b458038..fddf843f10 100644
--- a/src/graph-theory/walks-finite-undirected-graphs.lagda.md
+++ b/src/graph-theory/walks-finite-undirected-graphs.lagda.md
@@ -1,6 +1,8 @@
 # Walks in finite undirected graphs
 
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module graph-theory.walks-finite-undirected-graphs where
 ```
 
@@ -537,7 +539,6 @@ module _
     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/organic-chemistry/ethane.lagda.md b/src/organic-chemistry/ethane.lagda.md
index 74afce7451..90b33afc99 100644
--- a/src/organic-chemistry/ethane.lagda.md
+++ b/src/organic-chemistry/ethane.lagda.md
@@ -28,7 +28,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/finite-undirected-trees.lagda.md b/src/trees/finite-undirected-trees.lagda.md
index ab1c20340a..4341cdb996 100644
--- a/src/trees/finite-undirected-trees.lagda.md
+++ b/src/trees/finite-undirected-trees.lagda.md
@@ -1,6 +1,8 @@
 # Finite undirected trees
 
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module trees.finite-undirected-trees where
 ```
 
diff --git a/src/univalent-combinatorics/cyclic-types.lagda.md b/src/univalent-combinatorics/cyclic-types.lagda.md
index ddb8ce0019..bf37bf639b 100644
--- a/src/univalent-combinatorics/cyclic-types.lagda.md
+++ b/src/univalent-combinatorics/cyclic-types.lagda.md
@@ -1,6 +1,8 @@
 # Cyclic types
 
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module univalent-combinatorics.cyclic-types where
 ```
 
diff --git a/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md b/src/univalent-combinatorics/decidable-equivalence-relations.lagda.md
index f2d7d5fb87..d6f1108833 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/morphisms-cyclic-types.lagda.md b/src/univalent-combinatorics/morphisms-cyclic-types.lagda.md
index c827c99bca..b561f3daa1 100644
--- a/src/univalent-combinatorics/morphisms-cyclic-types.lagda.md
+++ b/src/univalent-combinatorics/morphisms-cyclic-types.lagda.md
@@ -1,6 +1,8 @@
 # Morphisms of cyclic types
 
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module univalent-combinatorics.morphisms-cyclic-types where
 ```
 
@@ -11,7 +13,7 @@ open import elementary-number-theory.natural-numbers
 
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
-open import foundation.functions
+open import foundation.function-types
 open import foundation.universe-levels
 
 open import univalent-combinatorics.cyclic-types
diff --git a/src/univalent-combinatorics/reduced-1-bordism-category.lagda.md b/src/univalent-combinatorics/reduced-1-bordism-category.lagda.md
index 0b752efee3..1a3932a189 100644
--- a/src/univalent-combinatorics/reduced-1-bordism-category.lagda.md
+++ b/src/univalent-combinatorics/reduced-1-bordism-category.lagda.md
@@ -1,6 +1,8 @@
 # The reduced 1-bordism category
 
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module univalent-combinatorics.reduced-1-bordism-category where
 ```
 

From d4ae7d0a1b11d854e5a325ef8192c26fa709b0c9 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sat, 17 Jun 2023 13:18:24 +0200
Subject: [PATCH 10/23] refactoring undirected graphs

---
 .../commuting-triangles-of-maps.lagda.md      |  17 +-
 .../symmetric-binary-relations.lagda.md       | 137 ++++++++++++-
 .../unordered-pairs-of-types.lagda.md         |   2 +-
 src/foundation/unordered-pairs.lagda.md       | 186 ++++++++++++++++--
 src/graph-theory.lagda.md                     |   3 +
 ...ected-graphs-to-undirected-graphs.lagda.md |  49 +++++
 ...irected-graphs-to-directed-graphs.lagda.md |  73 +++++++
 .../undirected-core-directed-graphs.lagda.md  |  51 +++++
 src/graph-theory/undirected-graphs.lagda.md   | 127 ++++++------
 .../descent-circle.lagda.md                   |  18 +-
 10 files changed, 554 insertions(+), 109 deletions(-)
 create mode 100644 src/graph-theory/forgetful-functor-from-directed-graphs-to-undirected-graphs.lagda.md
 create mode 100644 src/graph-theory/forgetful-functor-from-undirected-graphs-to-directed-graphs.lagda.md
 create mode 100644 src/graph-theory/undirected-core-directed-graphs.lagda.md

diff --git a/src/foundation/commuting-triangles-of-maps.lagda.md b/src/foundation/commuting-triangles-of-maps.lagda.md
index b1f54b0fe3..9ddf15431b 100644
--- a/src/foundation/commuting-triangles-of-maps.lagda.md
+++ b/src/foundation/commuting-triangles-of-maps.lagda.md
@@ -11,10 +11,12 @@ open import foundation-core.commuting-triangles-of-maps public
 ```agda
 open import foundation.action-on-identifications-functions
 open import foundation.functoriality-dependent-function-types
+open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.universe-levels
 
 open import foundation-core.equivalences
+open import foundation-core.function-types
 ```
 
 </details>
@@ -50,13 +52,22 @@ module _
 
   equiv-coherence-triangle-maps-inv-top :
     coherence-triangle-maps left right (map-equiv e) ≃
-    coherence-triangle-maps' right left (map-inv-equiv e)
+    coherence-triangle-maps right left (map-inv-equiv e)
   equiv-coherence-triangle-maps-inv-top =
-    equiv-Π
+    ( equiv-inv-htpy
+      ( left ∘ (map-inv-equiv e))
+      ( right)) ∘e
+    ( equiv-Π
       ( λ b → left (map-inv-equiv e b) ＝ right b)
       ( e)
       ( λ a →
         equiv-concat
           ( ap left (is-retraction-map-inv-equiv e a))
-          ( right (map-equiv e a)))
+          ( right (map-equiv e a))))
+
+  coherence-triangle-maps-inv-top :
+    coherence-triangle-maps left right (map-equiv e) →
+    coherence-triangle-maps right left (map-inv-equiv e)
+  coherence-triangle-maps-inv-top =
+    map-equiv equiv-coherence-triangle-maps-inv-top
 ```
diff --git a/src/foundation/symmetric-binary-relations.lagda.md b/src/foundation/symmetric-binary-relations.lagda.md
index d00278edd7..6a2f58e668 100644
--- a/src/foundation/symmetric-binary-relations.lagda.md
+++ b/src/foundation/symmetric-binary-relations.lagda.md
@@ -8,10 +8,22 @@ module foundation.symmetric-binary-relations where
 
 ```agda
 open import foundation.action-on-equivalences-type-families
+open import foundation.action-on-identifications-functions
+open import foundation.binary-relations
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.equivalence-extensionality
 open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.symmetric-operations
 open import foundation.transport
 open import foundation.universe-levels
 open import foundation.unordered-pairs
+
+open import univalent-combinatorics.standard-finite-types
 ```
 
 </details>
@@ -30,6 +42,10 @@ symmetric binary relation `R` on `A` and an equivalence of unordered pairs
 for any two elements `x y : A`, where `{x,y}` is the _standard unordered pair_
 consisting of `x` and `y`.
 
+Note that a symmetric binary relation R on a type is just a
+[symmetric operation](foundation.symmetric-operations.md) from `A` into a
+universe `𝒰`.
+
 ## Definitions
 
 ### Symmetric binary relations
@@ -37,23 +53,124 @@ consisting of `x` and `y`.
 ```agda
 symmetric-binary-relation :
   {l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
-symmetric-binary-relation l2 A = unordered-pair A → UU l2
+symmetric-binary-relation l2 A = symmetric-operation A (UU l2)
+```
+
+### Action on symmetries of symmetric binary relations
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : symmetric-binary-relation l2 A)
+  where
+
+  abstract
+    equiv-tr-symmetric-binary-relation :
+      (p q : unordered-pair A) → Eq-unordered-pair p q → R p ≃ R q
+    equiv-tr-symmetric-binary-relation p =
+      ind-Eq-unordered-pair p (λ q e → R p ≃ R q) id-equiv
+
+    compute-refl-equiv-tr-symmetric-binary-relation :
+      (p : unordered-pair A) →
+      equiv-tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p) ＝
+      id-equiv
+    compute-refl-equiv-tr-symmetric-binary-relation p =
+      compute-refl-ind-Eq-unordered-pair p (λ q e → R p ≃ R q) id-equiv
+
+    htpy-compute-refl-equiv-tr-symmetric-binary-relation :
+      (p : unordered-pair A) →
+      htpy-equiv
+        ( equiv-tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p))
+        ( id-equiv)
+    htpy-compute-refl-equiv-tr-symmetric-binary-relation p =
+      htpy-eq-equiv (compute-refl-equiv-tr-symmetric-binary-relation p)
+
+  abstract
+    tr-symmetric-binary-relation :
+      (p q : unordered-pair A) → Eq-unordered-pair p q → R p → R q
+    tr-symmetric-binary-relation p q e =
+      map-equiv (equiv-tr-symmetric-binary-relation p q e)
+
+    compute-refl-tr-symmetric-binary-relation :
+      (p : unordered-pair A) →
+      tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p) ＝ id
+    compute-refl-tr-symmetric-binary-relation p =
+      ap map-equiv (compute-refl-equiv-tr-symmetric-binary-relation p)
+
+    htpy-compute-refl-tr-symmetric-binary-relation :
+      (p : unordered-pair A) →
+      tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p) ~ id
+    htpy-compute-refl-tr-symmetric-binary-relation p =
+      htpy-eq (compute-refl-tr-symmetric-binary-relation p)
 ```
 
-### Symmetries of symmetric binary relations
+### The underlying binary relation of a symmetric binary relation
 
 ```agda
 module _
   {l1 l2 : Level} {A : UU l1} (R : symmetric-binary-relation l2 A)
   where
 
-  equiv-tr-symmetric-binary-relation :
-    (p q : unordered-pair A) → Eq-unordered-pair p q → R p ≃ R q
-  equiv-tr-symmetric-binary-relation p q e =
-    equiv-tr R (eq-Eq-unordered-pair' p q e)
+  rel-symmetric-binary-relation : Rel l2 A
+  rel-symmetric-binary-relation x y = R (standard-unordered-pair x y)
+
+  equiv-symmetric-rel-symmetric-binary-relation :
+    {x y : A} →
+    rel-symmetric-binary-relation x y ≃ rel-symmetric-binary-relation y x
+  equiv-symmetric-rel-symmetric-binary-relation {x} {y} =
+    equiv-tr-symmetric-binary-relation R
+      ( standard-unordered-pair x y)
+      ( standard-unordered-pair y x)
+      ( swap-standard-unordered-pair x y)
+
+  symmetric-rel-symmetric-binary-relation :
+    {x y : A} →
+    rel-symmetric-binary-relation x y → rel-symmetric-binary-relation y x
+  symmetric-rel-symmetric-binary-relation =
+    map-equiv equiv-symmetric-rel-symmetric-binary-relation
+```
+
+### The forgetful functor from binary relations to symmetric binary relations
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Rel l2 A)
+  where
+
+  symmetric-binary-relation-Rel : symmetric-binary-relation l2 A
+  symmetric-binary-relation-Rel p =
+    Σ ( type-unordered-pair p)
+      ( λ i →
+        R (element-unordered-pair p i) (other-element-unordered-pair p i))
+
+  unit-symmetric-binary-relation-Rel :
+    (x y : A) →
+    R x y → rel-symmetric-binary-relation symmetric-binary-relation-Rel x y
+  pr1 (unit-symmetric-binary-relation-Rel x y r) = zero-Fin 1
+  pr2 (unit-symmetric-binary-relation-Rel x y r) =
+    tr
+      ( R x)
+      ( inv (compute-other-element-standard-unordered-pair x y (zero-Fin 1)))
+      ( r)
+```
+
+### The symmetric core of a binary relation
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : Rel l2 A)
+  where
+
+  symmetric-core-Rel : symmetric-binary-relation l2 A
+  symmetric-core-Rel p =
+    (i : type-unordered-pair p) →
+    R (element-unordered-pair p i) (other-element-unordered-pair p i)
 
-  tr-symmetric-binary-relation :
-    (p q : unordered-pair A) → Eq-unordered-pair p q → R p → R q
-  tr-symmetric-binary-relation p q e =
-    map-equiv (equiv-tr-symmetric-binary-relation p q e)
+  counit-symmetric-core-Rel :
+    (x y : A) →
+    rel-symmetric-binary-relation symmetric-core-Rel x y → R x y
+  counit-symmetric-core-Rel x y r =
+    tr
+      ( R x)
+      ( compute-other-element-standard-unordered-pair x y (zero-Fin 1))
+      ( r (zero-Fin 1))
 ```
diff --git a/src/foundation/unordered-pairs-of-types.lagda.md b/src/foundation/unordered-pairs-of-types.lagda.md
index 6819cbe635..491d79e352 100644
--- a/src/foundation/unordered-pairs-of-types.lagda.md
+++ b/src/foundation/unordered-pairs-of-types.lagda.md
@@ -71,7 +71,7 @@ module _
 
 ## Properties
 
-### Univalence for unordered pairs of types
+### Extensionality of unordered pairs of types
 
 ```agda
 module _
diff --git a/src/foundation/unordered-pairs.lagda.md b/src/foundation/unordered-pairs.lagda.md
index 9846baf1a1..c3de4e1b57 100644
--- a/src/foundation/unordered-pairs.lagda.md
+++ b/src/foundation/unordered-pairs.lagda.md
@@ -8,6 +8,9 @@ module foundation.unordered-pairs where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.commuting-triangles-of-maps
+open import foundation.contractible-maps
+open import foundation.contractible-types
 open import foundation.decidable-equality
 open import foundation.dependent-pair-types
 open import foundation.existential-quantification
@@ -18,9 +21,9 @@ open import foundation.mere-equivalences
 open import foundation.propositional-truncations
 open import foundation.structure-identity-principle
 open import foundation.unit-type
+open import foundation.universal-property-dependent-pair-types
 open import foundation.universe-levels
 
-open import foundation-core.contractible-types
 open import foundation-core.coproduct-types
 open import foundation-core.embeddings
 open import foundation-core.equivalences
@@ -125,21 +128,34 @@ Any two elements `x` and `y` in a type `A` define a standard unordered pair
 
 ```agda
 module _
-  {l1 : Level} {A : UU l1}
+  {l1 : Level} {A : UU l1} (x y : A)
   where
 
-  element-standard-unordered-pair : (x y : A) → Fin 2 → A
-  element-standard-unordered-pair x y (inl (inr star)) = x
-  element-standard-unordered-pair x y (inr star) = y
-
-  standard-unordered-pair : A → A → unordered-pair A
-  pr1 (standard-unordered-pair x y) = Fin-UU-Fin' 2
-  pr2 (standard-unordered-pair x y) = element-standard-unordered-pair x y
+  element-standard-unordered-pair : Fin 2 → A
+  element-standard-unordered-pair (inl (inr star)) = x
+  element-standard-unordered-pair (inr star) = y
+
+  standard-unordered-pair : unordered-pair A
+  pr1 standard-unordered-pair = Fin-UU-Fin' 2
+  pr2 standard-unordered-pair = element-standard-unordered-pair
+
+  other-element-standard-unordered-pair : Fin 2 → A
+  other-element-standard-unordered-pair (inl (inr star)) = y
+  other-element-standard-unordered-pair (inr star) = x
+
+  compute-other-element-standard-unordered-pair :
+    (u : Fin 2) →
+    other-element-unordered-pair standard-unordered-pair u ＝
+    other-element-standard-unordered-pair u
+  compute-other-element-standard-unordered-pair (inl (inr star)) =
+    ap element-standard-unordered-pair (compute-swap-Fin-two-ℕ (inl (inr star)))
+  compute-other-element-standard-unordered-pair (inr star) =
+    ap element-standard-unordered-pair (compute-swap-Fin-two-ℕ (inr star))
 ```
 
 ## Properties
 
-### Equality of unordered pairs
+### Extensionality of unordered pairs
 
 ```agda
 module _
@@ -150,7 +166,10 @@ module _
   Eq-unordered-pair p q =
     Σ ( type-unordered-pair p ≃ type-unordered-pair q)
       ( λ e →
-        (element-unordered-pair p) ~ (element-unordered-pair q ∘ map-equiv e))
+        coherence-triangle-maps
+          ( element-unordered-pair p)
+          ( element-unordered-pair q)
+          ( map-equiv e))
 
   refl-Eq-unordered-pair : (p : unordered-pair A) → Eq-unordered-pair p p
   pr1 (refl-Eq-unordered-pair (pair X p)) = id-equiv-UU-Fin {k = 2} X
@@ -211,6 +230,78 @@ module _
   eq-Eq-refl-unordered-pair p = is-retraction-eq-Eq-unordered-pair p p refl
 ```
 
+### Induction on equality of unordered pairs
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (p : unordered-pair A)
+  (B : (q : unordered-pair A) → Eq-unordered-pair p q → UU l2)
+  where
+
+  ev-refl-Eq-unordered-pair :
+    ((q : unordered-pair A) (e : Eq-unordered-pair p q) → B q e) →
+    B p (refl-Eq-unordered-pair p)
+  ev-refl-Eq-unordered-pair f = f p (refl-Eq-unordered-pair p)
+
+  triangle-ev-refl-Eq-unordered-pair :
+    coherence-triangle-maps
+      ( ev-point (p , refl-Eq-unordered-pair p))
+      ( ev-refl-Eq-unordered-pair)
+      ( ev-pair)
+  triangle-ev-refl-Eq-unordered-pair = refl-htpy
+
+  abstract
+    is-equiv-ev-refl-Eq-unordered-pair : is-equiv ev-refl-Eq-unordered-pair
+    is-equiv-ev-refl-Eq-unordered-pair =
+      is-equiv-left-factor-htpy
+        ( ev-point (p , refl-Eq-unordered-pair p))
+        ( ev-refl-Eq-unordered-pair)
+        ( ev-pair)
+        ( triangle-ev-refl-Eq-unordered-pair)
+        ( dependent-universal-property-contr-is-contr
+          ( p , refl-Eq-unordered-pair p)
+          ( is-contr-total-Eq-unordered-pair p)
+          ( λ u → B (pr1 u) (pr2 u)))
+        ( is-equiv-ev-pair)
+
+  abstract
+    is-contr-map-ev-refl-Eq-unordered-pair :
+      is-contr-map ev-refl-Eq-unordered-pair
+    is-contr-map-ev-refl-Eq-unordered-pair =
+      is-contr-map-is-equiv is-equiv-ev-refl-Eq-unordered-pair
+
+  abstract
+    ind-Eq-unordered-pair :
+      B p (refl-Eq-unordered-pair p) →
+      ((q : unordered-pair A) (e : Eq-unordered-pair p q) → B q e)
+    ind-Eq-unordered-pair u =
+      pr1 (center (is-contr-map-ev-refl-Eq-unordered-pair u))
+
+    compute-refl-ind-Eq-unordered-pair :
+      (u : B p (refl-Eq-unordered-pair p)) →
+      ind-Eq-unordered-pair u p (refl-Eq-unordered-pair p) ＝ u
+    compute-refl-ind-Eq-unordered-pair u =
+      pr2 (center (is-contr-map-ev-refl-Eq-unordered-pair u))
+```
+
+### Inverting extensional equality of unordered pairs
+
+```agda
+module _
+  {l : Level} {A : UU l} (p q : unordered-pair A)
+  where
+
+  inv-Eq-unordered-pair :
+    Eq-unordered-pair p q → Eq-unordered-pair q p
+  pr1 (inv-Eq-unordered-pair (e , H)) = inv-equiv e
+  pr2 (inv-Eq-unordered-pair (e , H)) =
+    coherence-triangle-maps-inv-top
+      ( element-unordered-pair p)
+      ( element-unordered-pair q)
+      ( e)
+      ( H)
+```
+
 ### Mere equality of unordered pairs
 
 ```agda
@@ -238,15 +329,25 @@ module _
 ### A standard unordered pair `{x,y}` is equal to the standard unordered pair `{y,x}`
 
 ```agda
-is-commutative-standard-unordered-pair :
-  {l : Level} {A : UU l} (x y : A) →
-  standard-unordered-pair x y ＝ standard-unordered-pair y x
-is-commutative-standard-unordered-pair x y =
-  eq-Eq-unordered-pair
-    ( standard-unordered-pair x y)
-    ( standard-unordered-pair y x)
-    ( equiv-succ-Fin 2)
-    ( λ { (inl (inr star)) → refl ; (inr star) → refl})
+module _
+  {l1 : Level} {A : UU l1} (x y : A)
+  where
+
+  swap-standard-unordered-pair :
+    Eq-unordered-pair
+      ( standard-unordered-pair x y)
+      ( standard-unordered-pair y x)
+  pr1 swap-standard-unordered-pair = equiv-succ-Fin 2
+  pr2 swap-standard-unordered-pair (inl (inr star)) = refl
+  pr2 swap-standard-unordered-pair (inr star) = refl
+
+  is-commutative-standard-unordered-pair :
+    standard-unordered-pair x y ＝ standard-unordered-pair y x
+  is-commutative-standard-unordered-pair =
+    eq-Eq-unordered-pair'
+      ( standard-unordered-pair x y)
+      ( standard-unordered-pair y x)
+      ( swap-standard-unordered-pair)
 ```
 
 ### Functoriality of unordered pairs
@@ -372,3 +473,48 @@ is-surjective-standard-unordered-pair (I , a) =
             ( e)
             ( λ { (inl (inr star)) → refl ; (inr star) → refl})))
 ```
+
+### For every unordered pair `p` and every element `i` in its underlying type, `p` is equal to a standard unordered pair
+
+```agda
+module _
+  {l : Level} {A : UU l} (p : unordered-pair A) (i : type-unordered-pair p)
+  where
+
+  compute-standard-unordered-pair-element-unordered-pair :
+    Eq-unordered-pair
+      ( standard-unordered-pair
+        ( element-unordered-pair p i)
+        ( other-element-unordered-pair p i))
+      ( p)
+  pr1 compute-standard-unordered-pair-element-unordered-pair =
+    equiv-point-2-Element-Type
+      ( 2-element-type-unordered-pair p)
+      ( i)
+  pr2 compute-standard-unordered-pair-element-unordered-pair (inl (inr star)) =
+    ap
+      ( element-unordered-pair p)
+      ( inv
+        ( compute-map-equiv-point-2-Element-Type
+          ( 2-element-type-unordered-pair p)
+          ( i)))
+  pr2 compute-standard-unordered-pair-element-unordered-pair (inr star) =
+    ap
+      ( element-unordered-pair p)
+      ( inv
+        ( compute-map-equiv-point-2-Element-Type'
+          ( 2-element-type-unordered-pair p)
+          ( i)))
+
+  eq-compute-standard-unordered-pair-element-unordered-pair :
+    standard-unordered-pair
+      ( element-unordered-pair p i)
+      ( other-element-unordered-pair p i) ＝ p
+  eq-compute-standard-unordered-pair-element-unordered-pair =
+    eq-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)
+```
diff --git a/src/graph-theory.lagda.md b/src/graph-theory.lagda.md
index 5d22b843ae..24b9804638 100644
--- a/src/graph-theory.lagda.md
+++ b/src/graph-theory.lagda.md
@@ -26,6 +26,8 @@ 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-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,6 +47,7 @@ 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
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..418092447e
--- /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
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.symmetric-binary-relations
+open import foundation.universe-levels
+
+open import graph-theory.directed-graphs
+open import graph-theory.undirected-graphs
+```
+
+</details>
+
+## Idea
+
+The **forgetful functor** from
+[directed graphs](graph-theory.directed-graphs.md) to
+[undirected graphs](graph-theory.undirected-graphs.md) forgets the direction of
+directed edges.
+
+## Definitions
+
+### The operation on directed graphs that forgets the directions of the edges
+
+```agda
+module _
+  {l1 l2 : Level} (G : Directed-Graph l1 l2)
+  where
+
+  vertex-undirected-graph-Directed-Graph : UU l1
+  vertex-undirected-graph-Directed-Graph = vertex-Directed-Graph G
+
+  edge-undirected-graph-Directed-Graph :
+    symmetric-binary-relation l2 vertex-undirected-graph-Directed-Graph
+  edge-undirected-graph-Directed-Graph =
+    symmetric-binary-relation-Rel (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
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+open import foundation.unordered-pairs
+
+open import graph-theory.directed-graphs
+open import graph-theory.undirected-graphs
+```
+
+</details>
+
+## Idea
+
+The **forgetful functor** from
+[undirected graphs](graph-theory.undirected-graphs.md) to
+[directed graphs](graph-theory.directed-graphs.md) takes an undirected graph `G`
+and returns the directed graphs in which we have an edge from both `x` to `y`
+and from `y` to `x` for every undirected edge on the
+[standard unordered pair](foundation.unordered-pairs.md) `{x,y}`.
+
+## Definitions
+
+### The forgetful functor from undirected graphs to directed graphs
+
+```agda
+module _
+  {l1 l2 : Level} (G : Undirected-Graph l1 l2)
+  where
+
+  vertex-graph-Undirected-Graph : UU l1
+  vertex-graph-Undirected-Graph = vertex-Undirected-Graph G
+
+  edge-graph-Undirected-Graph :
+    (x y : vertex-graph-Undirected-Graph) → UU l2
+  edge-graph-Undirected-Graph x y =
+    edge-Undirected-Graph G (standard-unordered-pair x y)
+
+  graph-Undirected-Graph : Directed-Graph l1 l2
+  pr1 graph-Undirected-Graph = vertex-graph-Undirected-Graph
+  pr2 graph-Undirected-Graph = edge-graph-Undirected-Graph
+
+  directed-edge-edge-Undirected-Graph :
+    (p : unordered-pair-vertices-Undirected-Graph G)
+    (e : edge-Undirected-Graph G p)
+    (i : type-unordered-pair p) →
+    edge-graph-Undirected-Graph
+      ( element-unordered-pair p i)
+      ( other-element-unordered-pair p i)
+  directed-edge-edge-Undirected-Graph p e i =
+    tr-edge-Undirected-Graph G
+      ( p)
+      ( standard-unordered-pair
+        ( element-unordered-pair p i)
+        ( other-element-unordered-pair p i))
+      ( inv-Eq-unordered-pair
+        ( standard-unordered-pair
+          ( element-unordered-pair p i)
+          ( other-element-unordered-pair p i))
+        ( p)
+        ( compute-standard-unordered-pair-element-unordered-pair p i))
+      ( e)
+```
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..6c600507dd
--- /dev/null
+++ b/src/graph-theory/undirected-core-directed-graphs.lagda.md
@@ -0,0 +1,51 @@
+# The undirected core of a directed graph
+
+```agda
+module graph-theory.undirected-core-directed-graphs where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.symmetric-binary-relations
+open import foundation.universe-levels
+
+open import graph-theory.directed-graphs
+open import graph-theory.undirected-graphs
+```
+
+</details>
+
+## Idea
+
+The **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-binary-relation l2 vertex-undirected-core-Directed-Graph
+  edge-undirected-core-Directed-Graph =
+    symmetric-core-Rel (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
+```
diff --git a/src/graph-theory/undirected-graphs.lagda.md b/src/graph-theory/undirected-graphs.lagda.md
index 90ac67956c..38c00d06f5 100644
--- a/src/graph-theory/undirected-graphs.lagda.md
+++ b/src/graph-theory/undirected-graphs.lagda.md
@@ -11,8 +11,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
 open import foundation.universe-levels
 open import foundation.unordered-pairs
@@ -24,14 +28,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 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-binary-relation l2)
 
 module _
   {l1 l2 : Level} (G : Undirected-Graph l1 l2)
@@ -53,76 +66,50 @@ 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-binary-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
-
-  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 = {!!}
-```
-
-### 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-binary-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-binary-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-binary-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-binary-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-binary-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-binary-relation edge-Undirected-Graph
 ```
diff --git a/src/synthetic-homotopy-theory/descent-circle.lagda.md b/src/synthetic-homotopy-theory/descent-circle.lagda.md
index 1efe950f82..cdb73f89c0 100644
--- a/src/synthetic-homotopy-theory/descent-circle.lagda.md
+++ b/src/synthetic-homotopy-theory/descent-circle.lagda.md
@@ -460,11 +460,19 @@ module _
     hom-descent-data-circle l P Q
   equiv-fixpoint-descent-data-circle-function-type-hom =
     equiv-tot
-      (λ h →
-        ( equiv-inv-htpy (((map-equiv f) ∘ h)) (h ∘ (map-equiv e))) ∘e
-        ( ( inv-equiv
-            ( equiv-coherence-triangle-maps-inv-top ((map-equiv f) ∘ h) h e)) ∘e
-          ( equiv-funext)))
+      ( λ h →
+        ( inv-equiv
+          ( ( equiv-inv-htpy
+              ( h)
+              ( (map-equiv f ∘ h) ∘ map-inv-equiv e)) ∘e
+            ( ( equiv-coherence-triangle-maps-inv-top
+                ( (map-equiv f) ∘ h)
+                ( h)
+                ( e)) ∘e
+              ( equiv-inv-htpy
+                ( h ∘ map-equiv e)
+                ( map-equiv f ∘ h))))) ∘e
+        ( equiv-funext))
 
   equiv-ev-descent-data-circle-function-type-hom :
     dependent-universal-property-circle (l2 ⊔ l3) l →

From 0e9959d74f06718e6f9b636e90a3b616318211f1 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 18 Jun 2023 12:21:30 +0200
Subject: [PATCH 11/23] work

---
 src/foundation/binary-relations.lagda.md      | 11 +++
 .../equivalence-extensionality.lagda.md       | 33 ++++++++
 src/foundation/equivalence-induction.lagda.md | 63 +++++++--------
 src/foundation/equivalences.lagda.md          | 32 --------
 src/foundation/homotopies.lagda.md            |  4 +-
 src/foundation/identity-systems.lagda.md      | 52 +++++++------
 .../symmetric-binary-relations.lagda.md       | 78 ++++++++++++++++++-
 .../undirected-core-directed-graphs.lagda.md  | 31 ++++++++
 src/graph-theory/undirected-graphs.lagda.md   |  2 -
 9 files changed, 213 insertions(+), 93 deletions(-)

diff --git a/src/foundation/binary-relations.lagda.md b/src/foundation/binary-relations.lagda.md
index ea164bc006..1c922eb530 100644
--- a/src/foundation/binary-relations.lagda.md
+++ b/src/foundation/binary-relations.lagda.md
@@ -118,6 +118,17 @@ is-prop-is-transitive-Rel-Prop R =
                 ( is-prop-function-type (is-prop-type-Rel-Prop R x z)))))
 ```
 
+### Morphisms of binary relations
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1}
+  where
+
+  hom-Rel : Rel l2 A → Rel l3 A → UU (l1 ⊔ l2 ⊔ l3)
+  hom-Rel R S = (x y : A) → R x y → S x y
+```
+
 ## Properties
 
 ### Characterization of equality of binary relations
diff --git a/src/foundation/equivalence-extensionality.lagda.md b/src/foundation/equivalence-extensionality.lagda.md
index b3c231ac85..6ab0910047 100644
--- a/src/foundation/equivalence-extensionality.lagda.md
+++ b/src/foundation/equivalence-extensionality.lagda.md
@@ -10,6 +10,7 @@ module foundation.equivalence-extensionality where
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.fundamental-theorem-of-identity-types
+open import foundation.identity-systems
 open import foundation.subtype-identity-principle
 open import foundation.type-theoretic-principle-of-choice
 open import foundation.universe-levels
@@ -24,6 +25,7 @@ open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.propositions
+open import foundation-core.sections
 ```
 
 </details>
@@ -86,3 +88,34 @@ module _
     {e e' : A ≃ B} → (map-equiv e) ＝ (map-equiv e') → htpy-equiv e e'
   htpy-eq-map-equiv = htpy-eq
 ```
+
+### Homotopy induction for homotopies between equivalences
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  abstract
+    Ind-htpy-equiv :
+      {l3 : Level} (e : A ≃ B)
+      (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) →
+      section
+        ( λ (h : (e' : A ≃ B) (H : htpy-equiv e e') → P e' H) →
+          h e (refl-htpy-equiv e))
+    Ind-htpy-equiv e =
+      is-identity-system-is-torsorial-family-of-types e
+        ( refl-htpy-equiv e)
+        ( is-contr-total-htpy-equiv e)
+
+  ind-htpy-equiv :
+    {l3 : Level} (e : A ≃ B) (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) →
+    P e (refl-htpy-equiv e) → (e' : A ≃ B) (H : htpy-equiv e e') → P e' H
+  ind-htpy-equiv e P = pr1 (Ind-htpy-equiv e P)
+
+  compute-ind-htpy-equiv :
+    {l3 : Level} (e : A ≃ B) (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3)
+    (p : P e (refl-htpy-equiv e)) →
+    ind-htpy-equiv e P p e (refl-htpy-equiv e) ＝ p
+  compute-ind-htpy-equiv e P = pr2 (Ind-htpy-equiv e P)
+```
diff --git a/src/foundation/equivalence-induction.lagda.md b/src/foundation/equivalence-induction.lagda.md
index 1682243778..89cf898ae1 100644
--- a/src/foundation/equivalence-induction.lagda.md
+++ b/src/foundation/equivalence-induction.lagda.md
@@ -73,8 +73,8 @@ module _
     {l : Level}
     (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) →
     coherence-triangle-maps
-      ( ev-point (pair A id-equiv) {P})
-      ( ev-id-equiv (λ X e → P (pair X e)))
+      ( ev-point (A , id-equiv) {P})
+      ( ev-id-equiv (λ X e → P (X , e)))
       ( ev-pair {A = UU l1} {B = λ X → A ≃ X} {C = P})
   triangle-ev-id-equiv P f = refl
 ```
@@ -91,20 +91,19 @@ module _
   where
 
   abstract
-    IND-EQUIV-is-contr-total-equiv :
+    is-identity-system-is-contr-total-equiv :
       is-contr (Σ (UU l1) (λ X → A ≃ X)) →
       {l : Level} →
-      (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) → IND-EQUIV (λ B e → P (pair B e))
-    IND-EQUIV-is-contr-total-equiv c P =
+      (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) → IND-EQUIV (λ B e → P (B , e))
+    is-identity-system-is-contr-total-equiv c P =
       section-left-factor
-        ( ev-id-equiv (λ X e → P (pair X e)))
+        ( ev-id-equiv (λ X e → P (X , e)))
         ( ev-pair)
         ( is-singleton-is-contr
-          ( pair A id-equiv)
-          ( pair
-            ( pair A id-equiv)
-            ( λ t → ( inv (contraction c (pair A id-equiv))) ∙
-                    ( contraction c t)))
+          ( A , id-equiv)
+          ( ( A , id-equiv) ,
+            ( λ t →
+              ( inv (contraction c (A , id-equiv))) ∙ (contraction c t)))
           ( P))
 ```
 
@@ -116,19 +115,18 @@ module _
   where
 
   abstract
-    is-contr-total-equiv-IND-EQUIV :
-      ( {l : Level} (P : (Σ (UU l1) (λ X → A ≃ X)) → UU l) →
-        IND-EQUIV (λ B e → P (pair B e))) →
+    is-contr-total-is-identity-system-equiv :
+      ( {l : Level} → is-identity-system l (λ X → A ≃ X) A id-equiv) →
       is-contr (Σ (UU l1) (λ X → A ≃ X))
-    is-contr-total-equiv-IND-EQUIV ind =
+    is-contr-total-is-identity-system-equiv ind =
       is-contr-is-singleton
         ( Σ (UU l1) (λ X → A ≃ X))
-        ( pair A id-equiv)
+        ( A , id-equiv)
         ( λ P → section-comp
-          ( ev-id-equiv (λ X e → P (pair X e)))
+          ( ev-id-equiv (λ X e → P (X , e)))
           ( ev-pair {A = UU l1} {B = λ X → A ≃ X} {C = P})
-          ( pair ind-Σ refl-htpy)
-          ( ind P))
+          ( ind-Σ , refl-htpy)
+          ( ind (λ X e → P (X , e))))
 ```
 
 ### Equivalence induction in a universe
@@ -139,19 +137,19 @@ module _
   where
 
   abstract
-    Ind-equiv : section (ev-id-equiv P)
-    Ind-equiv =
-      IND-EQUIV-is-contr-total-equiv
-      ( is-contr-total-equiv _)
-      ( λ t → P (pr1 t) (pr2 t))
+    is-identity-system-equiv : section (ev-id-equiv P)
+    is-identity-system-equiv =
+      is-identity-system-is-contr-total-equiv
+        ( is-contr-total-equiv _)
+        ( λ t → P (pr1 t) (pr2 t))
 
   ind-equiv :
     P A id-equiv → {B : UU l1} (e : A ≃ B) → P B e
-  ind-equiv p {B} = pr1 Ind-equiv p B
+  ind-equiv p {B} = pr1 is-identity-system-equiv p B
 
   compute-ind-equiv :
     (u : P A id-equiv) → ind-equiv u id-equiv ＝ u
-  compute-ind-equiv = pr2 Ind-equiv
+  compute-ind-equiv = pr2 is-identity-system-equiv
 ```
 
 ### Equivalence induction in a subuniverse
@@ -176,23 +174,26 @@ module _
   triangle-ev-id-equiv-subuniverse F E = refl
 
   abstract
-    Ind-equiv-subuniverse :
+    is-identity-system-equiv-subuniverse :
       (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) →
       section (ev-id-equiv-subuniverse {F})
-    Ind-equiv-subuniverse =
-      Ind-identity-system A id-equiv (is-contr-total-equiv-subuniverse P A)
+    is-identity-system-equiv-subuniverse =
+      is-identity-system-is-torsorial-family-of-types A id-equiv
+        ( is-contr-total-equiv-subuniverse P A)
 
   ind-equiv-subuniverse :
     (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) →
     F A id-equiv → (B : type-subuniverse P) (e : equiv-subuniverse P A B) →
     F B e
-  ind-equiv-subuniverse F = pr1 (Ind-equiv-subuniverse F)
+  ind-equiv-subuniverse F =
+    pr1 (is-identity-system-equiv-subuniverse F)
 
   compute-ind-equiv-subuniverse :
     (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) →
     (u : F A id-equiv) →
     ind-equiv-subuniverse F u A id-equiv ＝ u
-  compute-ind-equiv-subuniverse F = pr2 (Ind-equiv-subuniverse F)
+  compute-ind-equiv-subuniverse F =
+    pr2 (is-identity-system-equiv-subuniverse F)
 ```
 
 ### The evaluation map `ev-id-equiv` is an equivalence
diff --git a/src/foundation/equivalences.lagda.md b/src/foundation/equivalences.lagda.md
index ae1f1e6ca5..e328939b12 100644
--- a/src/foundation/equivalences.lagda.md
+++ b/src/foundation/equivalences.lagda.md
@@ -15,7 +15,6 @@ open import foundation.dependent-pair-types
 open import foundation.equivalence-extensionality
 open import foundation.function-extensionality
 open import foundation.functoriality-fibers-of-maps
-open import foundation.identity-systems
 open import foundation.identity-types
 open import foundation.truncated-maps
 open import foundation.type-theoretic-principle-of-choice
@@ -337,37 +336,6 @@ module _
   pr2 emb-map-equiv = is-emb-map-equiv
 ```
 
-### Homotopy induction for homotopies between equivalences
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
-  where
-
-  abstract
-    Ind-htpy-equiv :
-      {l3 : Level} (e : A ≃ B)
-      (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) →
-      section
-        ( λ (h : (e' : A ≃ B) (H : htpy-equiv e e') → P e' H) →
-          h e (refl-htpy-equiv e))
-    Ind-htpy-equiv e =
-      Ind-identity-system e
-        ( refl-htpy-equiv e)
-        ( is-contr-total-htpy-equiv e)
-
-  ind-htpy-equiv :
-    {l3 : Level} (e : A ≃ B) (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) →
-    P e (refl-htpy-equiv e) → (e' : A ≃ B) (H : htpy-equiv e e') → P e' H
-  ind-htpy-equiv e P = pr1 (Ind-htpy-equiv e P)
-
-  compute-ind-htpy-equiv :
-    {l3 : Level} (e : A ≃ B) (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3)
-    (p : P e (refl-htpy-equiv e)) →
-    ind-htpy-equiv e P p e (refl-htpy-equiv e) ＝ p
-  compute-ind-htpy-equiv e P = pr2 (Ind-htpy-equiv e P)
-```
-
 ### The groupoid laws for equivalences
 
 ```agda
diff --git a/src/foundation/homotopies.lagda.md b/src/foundation/homotopies.lagda.md
index 9ca7f628db..f8df9cf65a 100644
--- a/src/foundation/homotopies.lagda.md
+++ b/src/foundation/homotopies.lagda.md
@@ -84,7 +84,7 @@ abstract
     {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) →
     FUNEXT f → IND-HTPY {l3 = l3} f
   IND-HTPY-FUNEXT {l3 = l3} {A = A} {B = B} f funext-f =
-    Ind-identity-system f
+    is-identity-system-is-torsorial-family-of-types f
       ( refl-htpy)
       ( is-contr-total-htpy f)
 
@@ -93,7 +93,7 @@ abstract
     {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) →
     ({l : Level} → IND-HTPY {l3 = l} f) → FUNEXT f
   FUNEXT-IND-HTPY f ind-htpy-f =
-    fundamental-theorem-id-IND-identity-system f
+    fundamental-theorem-id-is-identity-system f
       ( refl-htpy)
       ( ind-htpy-f)
       ( λ g → htpy-eq)
diff --git a/src/foundation/identity-systems.lagda.md b/src/foundation/identity-systems.lagda.md
index da6502913b..5a2d0fdfb5 100644
--- a/src/foundation/identity-systems.lagda.md
+++ b/src/foundation/identity-systems.lagda.md
@@ -23,25 +23,29 @@ open import foundation-core.transport
 
 ## Idea
 
-A unary identity system on a type `A` equipped with a point `a : A` consists of
+A **(unary) identity system** on a type `A` equipped with a point `a : A` consists of
 a type family `B` over `A` equipped with a point `b : B a` that satisfies an
-induction principle analogous to the induction principle of the identity type at
-`a`.
+induction principle analogous to the induction principle of the [identity type](foundation.identity-types.md) at
+`a`. The [dependent universal property of identity types](foundation.universal-property-identity-types.md) also follows for identity systems.
+
+## Definitions
 
 ```agda
 module _
   {l1 l2 : Level} (l : Level) {A : UU l1} (B : A → UU l2) (a : A) (b : B a)
   where
 
-  IND-identity-system : UU (l1 ⊔ l2 ⊔ lsuc l)
-  IND-identity-system =
+  is-identity-system : UU (l1 ⊔ l2 ⊔ lsuc l)
+  is-identity-system =
     ( P : (x : A) (y : B x) → UU l) →
       section (λ (h : (x : A) (y : B x) → P x y) → h a b)
 ```
 
 ## Properties
 
-### A type family over `A` is an identity system if and only if it is equivalent to the identity type
+### A type family over `A` is an identity system if and only if its total space is contractible
+
+In [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md) we will start calling type families with contractible total space torsorial.
 
 ```agda
 module _
@@ -49,36 +53,36 @@ module _
   where
 
   abstract
-    Ind-identity-system :
-      (is-contr-AB : is-contr (Σ A B)) →
-      {l : Level} → IND-identity-system l B a b
-    pr1 (Ind-identity-system is-contr-AB P) p x y =
+    is-identity-system-is-torsorial-family-of-types :
+      (H : is-contr (Σ A B)) →
+      {l : Level} → is-identity-system l B a b
+    pr1 (is-identity-system-is-torsorial-family-of-types H P) p x y =
       tr
         ( fam-Σ P)
-        ( eq-is-contr is-contr-AB)
+        ( eq-is-contr H)
         ( p)
-    pr2 (Ind-identity-system is-contr-AB P) p =
+    pr2 (is-identity-system-is-torsorial-family-of-types H P) p =
       ap
         ( λ t → tr (fam-Σ P) t p)
         ( eq-is-contr'
-          ( is-prop-is-contr is-contr-AB (pair a b) (pair a b))
-          ( eq-is-contr is-contr-AB)
+          ( is-prop-is-contr H (pair a b) (pair a b))
+          ( eq-is-contr H)
           ( refl))
 
   abstract
-    is-contr-total-space-IND-identity-system :
-      ({l : Level} → IND-identity-system l B a b) → is-contr (Σ A B)
-    pr1 (pr1 (is-contr-total-space-IND-identity-system ind)) = a
-    pr2 (pr1 (is-contr-total-space-IND-identity-system ind)) = b
-    pr2 (is-contr-total-space-IND-identity-system ind) (pair x y) =
-      pr1 (ind (λ x' y' → (pair a b) ＝ (pair x' y'))) refl x y
+    is-torsorial-family-of-types-is-identity-system :
+      ({l : Level} → is-identity-system l B a b) → is-contr (Σ A B)
+    pr1 (pr1 (is-torsorial-family-of-types-is-identity-system H)) = a
+    pr2 (pr1 (is-torsorial-family-of-types-is-identity-system H)) = b
+    pr2 (is-torsorial-family-of-types-is-identity-system H) (pair x y) =
+      pr1 (H (λ x' y' → (pair a b) ＝ (pair x' y'))) refl x y
 
   abstract
-    fundamental-theorem-id-IND-identity-system :
-      ({l : Level} → IND-identity-system l B a b) →
+    fundamental-theorem-id-is-identity-system :
+      ({l : Level} → is-identity-system l B a b) →
       (f : (x : A) → a ＝ x → B x) → (x : A) → is-equiv (f x)
-    fundamental-theorem-id-IND-identity-system ind f =
+    fundamental-theorem-id-is-identity-system H f =
       fundamental-theorem-id
-        ( is-contr-total-space-IND-identity-system ind)
+        ( is-torsorial-family-of-types-is-identity-system H)
         ( f)
 ```
diff --git a/src/foundation/symmetric-binary-relations.lagda.md b/src/foundation/symmetric-binary-relations.lagda.md
index 6a2f58e668..a732178c5b 100644
--- a/src/foundation/symmetric-binary-relations.lagda.md
+++ b/src/foundation/symmetric-binary-relations.lagda.md
@@ -1,6 +1,8 @@
 # Symmetric binary relations
 
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module foundation.symmetric-binary-relations where
 ```
 
@@ -166,11 +168,83 @@ module _
     R (element-unordered-pair p i) (other-element-unordered-pair p i)
 
   counit-symmetric-core-Rel :
-    (x y : A) →
+    {x y : A} →
     rel-symmetric-binary-relation symmetric-core-Rel x y → R x y
-  counit-symmetric-core-Rel x y r =
+  counit-symmetric-core-Rel {x} {y} r =
     tr
       ( R x)
       ( compute-other-element-standard-unordered-pair x y (zero-Fin 1))
       ( r (zero-Fin 1))
 ```
+
+### Morphisms of symmetric binary relations
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1}
+  where
+
+  hom-symmetric-binary-relation :
+    symmetric-binary-relation l2 A → symmetric-binary-relation l3 A →
+    UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3)
+  hom-symmetric-binary-relation R S =
+    (p : unordered-pair A) → R p → S p
+
+  hom-rel-hom-symmetric-binary-relation :
+    (R : symmetric-binary-relation l2 A) (S : symmetric-binary-relation l3 A) →
+    hom-symmetric-binary-relation R S →
+    hom-Rel
+      ( rel-symmetric-binary-relation R)
+      ( rel-symmetric-binary-relation S)
+  hom-rel-hom-symmetric-binary-relation R S f x y =
+    f (standard-unordered-pair x y)
+```
+
+## Properties
+
+### The universal property of the symmetric core of a binary relation
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (R : Rel l2 A)
+  (S : symmetric-binary-relation l3 A)
+  where
+
+  map-universal-property-symmetric-core-Rel :
+    hom-symmetric-binary-relation S (symmetric-core-Rel R) →
+    hom-Rel (rel-symmetric-binary-relation S) R
+  map-universal-property-symmetric-core-Rel f x y s =
+    counit-symmetric-core-Rel R (f (standard-unordered-pair x y) s)
+
+  map-inv-universal-property-symmetric-core-Rel :
+    hom-Rel (rel-symmetric-binary-relation S) R →
+    hom-symmetric-binary-relation S (symmetric-core-Rel R)
+  map-inv-universal-property-symmetric-core-Rel f p s i =
+    f ( element-unordered-pair p i)
+      ( other-element-unordered-pair p i)
+      ( tr-symmetric-binary-relation S
+        ( 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))
+        ( s))
+
+  is-section-map-inv-universal-property-symmetric-core-Rel :
+    ( map-universal-property-symmetric-core-Rel ∘
+      map-inv-universal-property-symmetric-core-Rel) ~ id
+  is-section-map-inv-universal-property-symmetric-core-Rel f =
+    eq-htpy
+      ( λ p →
+        eq-htpy
+          ( λ s →
+            eq-htpy
+              ( λ i →
+                {!!})))
+    
+```
diff --git a/src/graph-theory/undirected-core-directed-graphs.lagda.md b/src/graph-theory/undirected-core-directed-graphs.lagda.md
index 6c600507dd..c27e88f8a6 100644
--- a/src/graph-theory/undirected-core-directed-graphs.lagda.md
+++ b/src/graph-theory/undirected-core-directed-graphs.lagda.md
@@ -8,10 +8,13 @@ module graph-theory.undirected-core-directed-graphs where
 
 ```agda
 open import foundation.dependent-pair-types
+open import foundation.function-types
 open import foundation.symmetric-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
 ```
 
@@ -49,3 +52,31 @@ module _
   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-Rel (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 38c00d06f5..c676feea72 100644
--- a/src/graph-theory/undirected-graphs.lagda.md
+++ b/src/graph-theory/undirected-graphs.lagda.md
@@ -1,8 +1,6 @@
 # Undirected graphs
 
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
-
 module graph-theory.undirected-graphs where
 ```
 

From b8bf006fec94695af8fc696712df1493275eabec Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 18 Jun 2023 12:22:16 +0200
Subject: [PATCH 12/23] make pre-commit

---
 src/foundation/identity-systems.lagda.md           | 13 ++++++++-----
 src/foundation/symmetric-binary-relations.lagda.md |  1 -
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/foundation/identity-systems.lagda.md b/src/foundation/identity-systems.lagda.md
index 5a2d0fdfb5..65a79e1635 100644
--- a/src/foundation/identity-systems.lagda.md
+++ b/src/foundation/identity-systems.lagda.md
@@ -23,10 +23,12 @@ open import foundation-core.transport
 
 ## Idea
 
-A **(unary) identity system** on a type `A` equipped with a point `a : A` consists of
-a type family `B` over `A` equipped with a point `b : B a` that satisfies an
-induction principle analogous to the induction principle of the [identity type](foundation.identity-types.md) at
-`a`. The [dependent universal property of identity types](foundation.universal-property-identity-types.md) also follows for identity systems.
+A **(unary) identity system** on a type `A` equipped with a point `a : A`
+consists of a type family `B` over `A` equipped with a point `b : B a` that
+satisfies an induction principle analogous to the induction principle of the
+[identity type](foundation.identity-types.md) at `a`. The
+[dependent universal property of identity types](foundation.universal-property-identity-types.md)
+also follows for identity systems.
 
 ## Definitions
 
@@ -45,7 +47,8 @@ module _
 
 ### A type family over `A` is an identity system if and only if its total space is contractible
 
-In [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md) we will start calling type families with contractible total space torsorial.
+In [`foundation.torsorial-type-families`](foundation.torsorial-type-families.md)
+we will start calling type families with contractible total space torsorial.
 
 ```agda
 module _
diff --git a/src/foundation/symmetric-binary-relations.lagda.md b/src/foundation/symmetric-binary-relations.lagda.md
index a732178c5b..da77068f39 100644
--- a/src/foundation/symmetric-binary-relations.lagda.md
+++ b/src/foundation/symmetric-binary-relations.lagda.md
@@ -246,5 +246,4 @@ module _
             eq-htpy
               ( λ i →
                 {!!})))
-    
 ```

From b5337f7216394c65f31b5f84f0e22ffe76bc7cb0 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Mon, 19 Jun 2023 14:08:02 +0200
Subject: [PATCH 13/23] fixes

---
 src/synthetic-homotopy-theory/suspensions-of-types.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index a0d46f594b..1e36cc17b4 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -211,7 +211,7 @@ module _
       P c' H)
   ind-htpy-suspension-structure P =
     pr1
-      ( Ind-identity-system
+      ( is-identity-system-is-torsorial-family-of-types
         ( c)
         ( refl-htpy-suspension-structure)
         ( is-contr-equiv

From 3ebbe9e8ad68585355091cae13d821cdc28b07d9 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Mon, 19 Jun 2023 17:16:55 +0200
Subject: [PATCH 14/23] the universal property of identity systems

---
 src/foundation.lagda.md                       |   1 +
 .../equivalence-extensionality.lagda.md       |   2 +-
 src/foundation/equivalence-induction.lagda.md |   2 +-
 src/foundation/homotopies.lagda.md            |   2 +-
 src/foundation/identity-systems.lagda.md      |  29 +++--
 ...iversal-property-identity-systems.lagda.md | 102 ++++++++++++++++++
 .../suspensions-of-types.lagda.md             |   2 +-
 7 files changed, 126 insertions(+), 14 deletions(-)
 create mode 100644 src/foundation/universal-property-identity-systems.lagda.md

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 54121fc69c..35c7c6fa0f 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -291,6 +291,7 @@ open import foundation.universal-property-coproduct-types public
 open import foundation.universal-property-dependent-pair-types public
 open import foundation.universal-property-empty-type public
 open import foundation.universal-property-fiber-products public
+open import foundation.universal-property-identity-systems public
 open import foundation.universal-property-identity-types public
 open import foundation.universal-property-image public
 open import foundation.universal-property-maybe public
diff --git a/src/foundation/equivalence-extensionality.lagda.md b/src/foundation/equivalence-extensionality.lagda.md
index 6ab0910047..b9ce4b187e 100644
--- a/src/foundation/equivalence-extensionality.lagda.md
+++ b/src/foundation/equivalence-extensionality.lagda.md
@@ -104,7 +104,7 @@ module _
         ( λ (h : (e' : A ≃ B) (H : htpy-equiv e e') → P e' H) →
           h e (refl-htpy-equiv e))
     Ind-htpy-equiv e =
-      is-identity-system-is-torsorial-family-of-types e
+      is-identity-system-is-torsorial e
         ( refl-htpy-equiv e)
         ( is-contr-total-htpy-equiv e)
 
diff --git a/src/foundation/equivalence-induction.lagda.md b/src/foundation/equivalence-induction.lagda.md
index 89cf898ae1..11fd12ad76 100644
--- a/src/foundation/equivalence-induction.lagda.md
+++ b/src/foundation/equivalence-induction.lagda.md
@@ -178,7 +178,7 @@ module _
       (F : (B : type-subuniverse P) → equiv-subuniverse P A B → UU l3) →
       section (ev-id-equiv-subuniverse {F})
     is-identity-system-equiv-subuniverse =
-      is-identity-system-is-torsorial-family-of-types A id-equiv
+      is-identity-system-is-torsorial A id-equiv
         ( is-contr-total-equiv-subuniverse P A)
 
   ind-equiv-subuniverse :
diff --git a/src/foundation/homotopies.lagda.md b/src/foundation/homotopies.lagda.md
index f8df9cf65a..0c02b432bc 100644
--- a/src/foundation/homotopies.lagda.md
+++ b/src/foundation/homotopies.lagda.md
@@ -84,7 +84,7 @@ abstract
     {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) →
     FUNEXT f → IND-HTPY {l3 = l3} f
   IND-HTPY-FUNEXT {l3 = l3} {A = A} {B = B} f funext-f =
-    is-identity-system-is-torsorial-family-of-types f
+    is-identity-system-is-torsorial f
       ( refl-htpy)
       ( is-contr-total-htpy f)
 
diff --git a/src/foundation/identity-systems.lagda.md b/src/foundation/identity-systems.lagda.md
index 65a79e1635..f43f47f342 100644
--- a/src/foundation/identity-systems.lagda.md
+++ b/src/foundation/identity-systems.lagda.md
@@ -1,6 +1,8 @@
 # Identity systems
 
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 module foundation.identity-systems where
 ```
 
@@ -32,15 +34,22 @@ also follows for identity systems.
 
 ## Definitions
 
+### The predicate of being an identity system
+
 ```agda
+ev-refl-identity-system :
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {a : A} (b : B a)
+  {P : (x : A) (y : B x) → UU l3} →
+  ((x : A) (y : B x) → P x y) → P a b
+ev-refl-identity-system b f = f _ b
+
 module _
   {l1 l2 : Level} (l : Level) {A : UU l1} (B : A → UU l2) (a : A) (b : B a)
   where
 
   is-identity-system : UU (l1 ⊔ l2 ⊔ lsuc l)
   is-identity-system =
-    ( P : (x : A) (y : B x) → UU l) →
-      section (λ (h : (x : A) (y : B x) → P x y) → h a b)
+    (P : (x : A) (y : B x) → UU l) → section (ev-refl-identity-system b {P})
 ```
 
 ## Properties
@@ -56,15 +65,15 @@ module _
   where
 
   abstract
-    is-identity-system-is-torsorial-family-of-types :
+    is-identity-system-is-torsorial :
       (H : is-contr (Σ A B)) →
       {l : Level} → is-identity-system l B a b
-    pr1 (is-identity-system-is-torsorial-family-of-types H P) p x y =
+    pr1 (is-identity-system-is-torsorial H P) p x y =
       tr
         ( fam-Σ P)
         ( eq-is-contr H)
         ( p)
-    pr2 (is-identity-system-is-torsorial-family-of-types H P) p =
+    pr2 (is-identity-system-is-torsorial H P) p =
       ap
         ( λ t → tr (fam-Σ P) t p)
         ( eq-is-contr'
@@ -73,11 +82,11 @@ module _
           ( refl))
 
   abstract
-    is-torsorial-family-of-types-is-identity-system :
+    is-torsorial-is-identity-system :
       ({l : Level} → is-identity-system l B a b) → is-contr (Σ A B)
-    pr1 (pr1 (is-torsorial-family-of-types-is-identity-system H)) = a
-    pr2 (pr1 (is-torsorial-family-of-types-is-identity-system H)) = b
-    pr2 (is-torsorial-family-of-types-is-identity-system H) (pair x y) =
+    pr1 (pr1 (is-torsorial-is-identity-system H)) = a
+    pr2 (pr1 (is-torsorial-is-identity-system H)) = b
+    pr2 (is-torsorial-is-identity-system H) (pair x y) =
       pr1 (H (λ x' y' → (pair a b) ＝ (pair x' y'))) refl x y
 
   abstract
@@ -86,6 +95,6 @@ module _
       (f : (x : A) → a ＝ x → B x) → (x : A) → is-equiv (f x)
     fundamental-theorem-id-is-identity-system H f =
       fundamental-theorem-id
-        ( is-torsorial-family-of-types-is-identity-system H)
+        ( is-torsorial-is-identity-system H)
         ( f)
 ```
diff --git a/src/foundation/universal-property-identity-systems.lagda.md b/src/foundation/universal-property-identity-systems.lagda.md
new file mode 100644
index 0000000000..0d427fc9c1
--- /dev/null
+++ b/src/foundation/universal-property-identity-systems.lagda.md
@@ -0,0 +1,102 @@
+# The universal property of identity systems
+
+```agda
+module foundation.universal-property-identity-systems where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.contractible-types
+open import foundation.dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.identity-systems
+open import foundation.torsorial-type-families
+open import foundation.universal-property-dependent-pair-types
+open import foundation.universe-levels
+
+open import foundation-core.equivalences
+open import foundation-core.identity-types
+open import foundation-core.sections
+open import foundation-core.transport
+```
+
+</details>
+
+## Idea
+
+A **(unary) identity system** on a type `A` equipped with a point `a : A`
+consists of a type family `B` over `A` equipped with a point `b : B a` that
+satisfies an induction principle analogous to the induction principle of the
+[identity type](foundation.identity-types.md) at `a`. The
+[dependent universal property of identity types](foundation.universal-property-identity-types.md)
+also follows for identity systems.
+
+## Definition
+
+### The universal property of identity systems
+
+```agda
+dependent-universal-property-identity-system :
+  {l1 l2 : Level} (l3 : Level) {A : UU l1} {B : A → UU l2} {a : A} (b : B a) →
+  UU (l1 ⊔ l2 ⊔ lsuc l3)
+dependent-universal-property-identity-system l3 {A} {B} b =
+  (P : (x : A) (y : B x) → UU l3) → is-equiv (ev-refl-identity-system b {P})
+```
+
+## Properties
+
+### A type family satisfies the dependent universal property of identity systems if and only if it is torsorial
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {a : A} (b : B a)
+  where
+
+  dependent-universal-property-identity-system-is-torsorial :
+    is-torsorial B →
+    {l3 : Level} → dependent-universal-property-identity-system l3 {A} {B} b
+  dependent-universal-property-identity-system-is-torsorial
+    H P =
+    is-equiv-left-factor
+      ( ev-refl-identity-system b)
+      ( ev-pair)
+      ( dependent-universal-property-contr-is-contr
+        ( a , b)
+        ( H)
+        ( λ u → P (pr1 u) (pr2 u)))
+      ( is-equiv-ev-pair)
+
+  is-torsorial-dependent-universal-property-identity-system :
+    ({l3 : Level} → dependent-universal-property-identity-system l3 {A} {B} b) →
+    is-torsorial B
+  pr1 (is-torsorial-dependent-universal-property-identity-system H) = (a , b)
+  pr2 (is-torsorial-dependent-universal-property-identity-system H) u =
+    map-inv-is-equiv
+      ( H (λ x y → (a , b) ＝ (x , y)))
+      ( refl)
+      ( pr1 u)
+      ( pr2 u)
+```
+
+### A type family satisfies the dependent universal property of identity systems if and only if it is an identity system
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {a : A} (b : B a)
+  where
+
+  dependent-universal-property-identity-system-is-identity-system :
+    ({l : Level} → is-identity-system l {A} B a b) →
+    ({l : Level} → dependent-universal-property-identity-system l {A} {B} b)
+  dependent-universal-property-identity-system-is-identity-system H =
+    dependent-universal-property-identity-system-is-torsorial b
+      ( is-torsorial-is-identity-system a b H)
+
+  is-identity-system-dependent-universal-property-identity-system :
+    ({l : Level} → dependent-universal-property-identity-system l {A} {B} b) →
+    ({l : Level} → is-identity-system l {A} B a b)
+  is-identity-system-dependent-universal-property-identity-system H P =
+    section-is-equiv (H P)
+```
diff --git a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
index 1e36cc17b4..7980b323d2 100644
--- a/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
+++ b/src/synthetic-homotopy-theory/suspensions-of-types.lagda.md
@@ -211,7 +211,7 @@ module _
       P c' H)
   ind-htpy-suspension-structure P =
     pr1
-      ( is-identity-system-is-torsorial-family-of-types
+      ( is-identity-system-is-torsorial
         ( c)
         ( refl-htpy-suspension-structure)
         ( is-contr-equiv

From b4b3e0079ddbcdfb5e7dec7133c8a353cc76db5d Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 21 Jun 2023 17:15:13 +0200
Subject: [PATCH 15/23] basic stuff about symmetric binary relations

---
 .../symmetric-binary-relations.lagda.md       | 32 +++++++++++++------
 1 file changed, 23 insertions(+), 9 deletions(-)

diff --git a/src/foundation/symmetric-binary-relations.lagda.md b/src/foundation/symmetric-binary-relations.lagda.md
index da77068f39..48b9f65ea6 100644
--- a/src/foundation/symmetric-binary-relations.lagda.md
+++ b/src/foundation/symmetric-binary-relations.lagda.md
@@ -92,6 +92,25 @@ module _
     tr-symmetric-binary-relation p q e =
       map-equiv (equiv-tr-symmetric-binary-relation p q e)
 
+    tr-inv-symmetric-binary-relation :
+      (p q : unordered-pair A) → Eq-unordered-pair p q → R q → R p
+    tr-inv-symmetric-binary-relation p q e =
+      map-inv-equiv (equiv-tr-symmetric-binary-relation p q e)
+
+    is-section-tr-inv-symmetric-binary-relation :
+      (p q : unordered-pair A) (e : Eq-unordered-pair p q) →
+      ( tr-symmetric-binary-relation p q e ∘
+        tr-inv-symmetric-binary-relation p q e) ~ id
+    is-section-tr-inv-symmetric-binary-relation p q e =
+      is-section-map-inv-equiv (equiv-tr-symmetric-binary-relation p q e)
+
+    is-retraction-tr-inv-symmetric-binary-relation :
+      (p q : unordered-pair A) (e : Eq-unordered-pair p q) →
+      ( tr-inv-symmetric-binary-relation p q e ∘
+        tr-symmetric-binary-relation p q e) ~ id
+    is-retraction-tr-inv-symmetric-binary-relation p q e =
+      is-retraction-map-inv-equiv (equiv-tr-symmetric-binary-relation p q e)
+
     compute-refl-tr-symmetric-binary-relation :
       (p : unordered-pair A) →
       tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p) ＝ id
@@ -222,17 +241,12 @@ module _
   map-inv-universal-property-symmetric-core-Rel f p s i =
     f ( element-unordered-pair p i)
       ( other-element-unordered-pair p i)
-      ( tr-symmetric-binary-relation S
-        ( p)
+      ( tr-inv-symmetric-binary-relation S
         ( 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))
+        ( p)
+        ( compute-standard-unordered-pair-element-unordered-pair p i)
         ( s))
 
   is-section-map-inv-universal-property-symmetric-core-Rel :
@@ -245,5 +259,5 @@ module _
           ( λ s →
             eq-htpy
               ( λ i →
-                {!!})))
+                {! !})))
 ```

From 197a987cd24c80c6fd559826c89bb7e2ad9ad369 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Mon, 11 Sep 2023 11:13:40 +0200
Subject: [PATCH 16/23] some fixes (not all)

---
 .../symmetric-binary-relations.lagda.md       | 85 ++++++++++---------
 ...ected-graphs-to-undirected-graphs.lagda.md |  2 +-
 .../undirected-core-directed-graphs.lagda.md  |  4 +-
 .../walks-undirected-graphs.lagda.md          |  2 +-
 .../suspension-structures.lagda.md            |  2 +-
 5 files changed, 48 insertions(+), 47 deletions(-)

diff --git a/src/foundation/symmetric-binary-relations.lagda.md b/src/foundation/symmetric-binary-relations.lagda.md
index 48b9f65ea6..af1a198db2 100644
--- a/src/foundation/symmetric-binary-relations.lagda.md
+++ b/src/foundation/symmetric-binary-relations.lagda.md
@@ -131,43 +131,44 @@ module _
   {l1 l2 : Level} {A : UU l1} (R : symmetric-binary-relation l2 A)
   where
 
-  rel-symmetric-binary-relation : Rel l2 A
-  rel-symmetric-binary-relation x y = R (standard-unordered-pair x y)
+  relation-symmetric-binary-relation : Relation l2 A
+  relation-symmetric-binary-relation x y = R (standard-unordered-pair x y)
 
-  equiv-symmetric-rel-symmetric-binary-relation :
+  equiv-symmetric-relation-symmetric-binary-relation :
     {x y : A} →
-    rel-symmetric-binary-relation x y ≃ rel-symmetric-binary-relation y x
-  equiv-symmetric-rel-symmetric-binary-relation {x} {y} =
+    relation-symmetric-binary-relation x y ≃ relation-symmetric-binary-relation y x
+  equiv-symmetric-relation-symmetric-binary-relation {x} {y} =
     equiv-tr-symmetric-binary-relation R
       ( standard-unordered-pair x y)
       ( standard-unordered-pair y x)
       ( swap-standard-unordered-pair x y)
 
-  symmetric-rel-symmetric-binary-relation :
+  symmetric-relation-symmetric-binary-relation :
     {x y : A} →
-    rel-symmetric-binary-relation x y → rel-symmetric-binary-relation y x
-  symmetric-rel-symmetric-binary-relation =
-    map-equiv equiv-symmetric-rel-symmetric-binary-relation
+    relation-symmetric-binary-relation x y →
+    relation-symmetric-binary-relation y x
+  symmetric-relation-symmetric-binary-relation =
+    map-equiv equiv-symmetric-relation-symmetric-binary-relation
 ```
 
 ### The forgetful functor from binary relations to symmetric binary relations
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} (R : Rel l2 A)
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
   where
 
-  symmetric-binary-relation-Rel : symmetric-binary-relation l2 A
-  symmetric-binary-relation-Rel p =
+  symmetric-binary-relation-Relation : symmetric-binary-relation l2 A
+  symmetric-binary-relation-Relation p =
     Σ ( type-unordered-pair p)
       ( λ i →
         R (element-unordered-pair p i) (other-element-unordered-pair p i))
 
-  unit-symmetric-binary-relation-Rel :
-    (x y : A) →
-    R x y → rel-symmetric-binary-relation symmetric-binary-relation-Rel x y
-  pr1 (unit-symmetric-binary-relation-Rel x y r) = zero-Fin 1
-  pr2 (unit-symmetric-binary-relation-Rel x y r) =
+  unit-symmetric-binary-relation-Relation :
+    (x y : A) → R x y →
+    relation-symmetric-binary-relation symmetric-binary-relation-Relation x y
+  pr1 (unit-symmetric-binary-relation-Relation x y r) = zero-Fin 1
+  pr2 (unit-symmetric-binary-relation-Relation x y r) =
     tr
       ( R x)
       ( inv (compute-other-element-standard-unordered-pair x y (zero-Fin 1)))
@@ -178,18 +179,18 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} (R : Rel l2 A)
+  {l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
   where
 
-  symmetric-core-Rel : symmetric-binary-relation l2 A
-  symmetric-core-Rel p =
+  symmetric-core-Relation : symmetric-binary-relation l2 A
+  symmetric-core-Relation p =
     (i : type-unordered-pair p) →
     R (element-unordered-pair p i) (other-element-unordered-pair p i)
 
-  counit-symmetric-core-Rel :
+  counit-symmetric-core-Relation :
     {x y : A} →
-    rel-symmetric-binary-relation symmetric-core-Rel x y → R x y
-  counit-symmetric-core-Rel {x} {y} r =
+    relation-symmetric-binary-relation symmetric-core-Relation x y → R x y
+  counit-symmetric-core-Relation {x} {y} r =
     tr
       ( R x)
       ( compute-other-element-standard-unordered-pair x y (zero-Fin 1))
@@ -209,13 +210,13 @@ module _
   hom-symmetric-binary-relation R S =
     (p : unordered-pair A) → R p → S p
 
-  hom-rel-hom-symmetric-binary-relation :
+  hom-relation-hom-symmetric-binary-relation :
     (R : symmetric-binary-relation l2 A) (S : symmetric-binary-relation l3 A) →
     hom-symmetric-binary-relation R S →
-    hom-Rel
-      ( rel-symmetric-binary-relation R)
-      ( rel-symmetric-binary-relation S)
-  hom-rel-hom-symmetric-binary-relation R S f x y =
+    hom-Relation
+      ( relation-symmetric-binary-relation R)
+      ( relation-symmetric-binary-relation S)
+  hom-relation-hom-symmetric-binary-relation R S f x y =
     f (standard-unordered-pair x y)
 ```
 
@@ -225,20 +226,20 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {A : UU l1} (R : Rel l2 A)
+  {l1 l2 l3 : Level} {A : UU l1} (R : Relation l2 A)
   (S : symmetric-binary-relation l3 A)
   where
 
-  map-universal-property-symmetric-core-Rel :
-    hom-symmetric-binary-relation S (symmetric-core-Rel R) →
-    hom-Rel (rel-symmetric-binary-relation S) R
-  map-universal-property-symmetric-core-Rel f x y s =
-    counit-symmetric-core-Rel R (f (standard-unordered-pair x y) s)
+  map-universal-property-symmetric-core-Relation :
+    hom-symmetric-binary-relation S (symmetric-core-Relation R) →
+    hom-Relation (relation-symmetric-binary-relation S) R
+  map-universal-property-symmetric-core-Relation f x y s =
+    counit-symmetric-core-Relation R (f (standard-unordered-pair x y) s)
 
-  map-inv-universal-property-symmetric-core-Rel :
-    hom-Rel (rel-symmetric-binary-relation S) R →
-    hom-symmetric-binary-relation S (symmetric-core-Rel R)
-  map-inv-universal-property-symmetric-core-Rel f p s i =
+  map-inv-universal-property-symmetric-core-Relation :
+    hom-Relation (relation-symmetric-binary-relation S) R →
+    hom-symmetric-binary-relation S (symmetric-core-Relation R)
+  map-inv-universal-property-symmetric-core-Relation f p s i =
     f ( element-unordered-pair p i)
       ( other-element-unordered-pair p i)
       ( tr-inv-symmetric-binary-relation S
@@ -249,10 +250,10 @@ module _
         ( compute-standard-unordered-pair-element-unordered-pair p i)
         ( s))
 
-  is-section-map-inv-universal-property-symmetric-core-Rel :
-    ( map-universal-property-symmetric-core-Rel ∘
-      map-inv-universal-property-symmetric-core-Rel) ~ id
-  is-section-map-inv-universal-property-symmetric-core-Rel f =
+  is-section-map-inv-universal-property-symmetric-core-Relation :
+    ( map-universal-property-symmetric-core-Relation ∘
+      map-inv-universal-property-symmetric-core-Relation) ~ id
+  is-section-map-inv-universal-property-symmetric-core-Relation f =
     eq-htpy
       ( λ p →
         eq-htpy
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
index 418092447e..47f67d15e8 100644
--- 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
@@ -41,7 +41,7 @@ module _
   edge-undirected-graph-Directed-Graph :
     symmetric-binary-relation l2 vertex-undirected-graph-Directed-Graph
   edge-undirected-graph-Directed-Graph =
-    symmetric-binary-relation-Rel (edge-Directed-Graph G)
+    symmetric-binary-relation-Relation (edge-Directed-Graph G)
 
   undirected-graph-Graph : Undirected-Graph l1 l2
   pr1 undirected-graph-Graph = vertex-undirected-graph-Directed-Graph
diff --git a/src/graph-theory/undirected-core-directed-graphs.lagda.md b/src/graph-theory/undirected-core-directed-graphs.lagda.md
index c27e88f8a6..1b53979d5f 100644
--- a/src/graph-theory/undirected-core-directed-graphs.lagda.md
+++ b/src/graph-theory/undirected-core-directed-graphs.lagda.md
@@ -46,7 +46,7 @@ module _
   edge-undirected-core-Directed-Graph :
     symmetric-binary-relation l2 vertex-undirected-core-Directed-Graph
   edge-undirected-core-Directed-Graph =
-    symmetric-core-Rel (edge-Directed-Graph G)
+    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
@@ -69,7 +69,7 @@ module _
     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-Rel (edge-Directed-Graph G)
+    counit-symmetric-core-Relation (edge-Directed-Graph G)
 
   counit-undirected-core-Directed-Graph :
     hom-Directed-Graph
diff --git a/src/graph-theory/walks-undirected-graphs.lagda.md b/src/graph-theory/walks-undirected-graphs.lagda.md
index 5f1e7f15bb..c7ed93e744 100644
--- a/src/graph-theory/walks-undirected-graphs.lagda.md
+++ b/src/graph-theory/walks-undirected-graphs.lagda.md
@@ -249,7 +249,7 @@ module _
     (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-has-inverse
+    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)
diff --git a/src/synthetic-homotopy-theory/suspension-structures.lagda.md b/src/synthetic-homotopy-theory/suspension-structures.lagda.md
index 58cf49bf18..ba72c9425e 100644
--- a/src/synthetic-homotopy-theory/suspension-structures.lagda.md
+++ b/src/synthetic-homotopy-theory/suspension-structures.lagda.md
@@ -259,7 +259,7 @@ module _
       P c' H)
   ind-htpy-suspension-structure P =
     pr1
-      ( Ind-identity-system
+      ( is-identity-system-is-torsorial
         ( c)
         ( refl-htpy-suspension-structure)
         ( is-contr-equiv

From f08ea0c968cfc61e3db2c115f88d405a9cbdc844 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 13 Sep 2023 13:18:57 +0200
Subject: [PATCH 17/23] make pre-commit

---
 src/foundation.lagda.md                                  | 1 +
 src/foundation/symmetric-cores-binary-relations.lagda.md | 9 +++++++--
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 606923be30..a507e62369 100644
--- a/src/foundation.lagda.md
+++ b/src/foundation.lagda.md
@@ -254,6 +254,7 @@ open import foundation.subtypes public
 open import foundation.subuniverses public
 open import foundation.surjective-maps public
 open import foundation.symmetric-binary-relations public
+open import foundation.symmetric-cores-binary-relations public
 open import foundation.symmetric-difference public
 open import foundation.symmetric-identity-types public
 open import foundation.symmetric-operations public
diff --git a/src/foundation/symmetric-cores-binary-relations.lagda.md b/src/foundation/symmetric-cores-binary-relations.lagda.md
index 12f31165d6..03808d4af9 100644
--- a/src/foundation/symmetric-cores-binary-relations.lagda.md
+++ b/src/foundation/symmetric-cores-binary-relations.lagda.md
@@ -42,13 +42,18 @@ that the precomposition function
   hom-Symmetric-Relation S (core R) → hom-Relation (rel S) R
 ```
 
-is an [equivalence](foundation-core.equivalences.md). The symmetric core of a binary relation `R` is defined as the relation
+is an [equivalence](foundation-core.equivalences.md). The symmetric core of a
+binary relation `R` is defined as the relation
 
 ```text
   core R (I,a) := (i : I) → R (a i) (a -i)
 ```
 
-where `-i` is the element of the [2-element type](univalent-combinatorics.2-element-types.md) obtained by applying the swap [involution](foundation.involutions.md) to `i`. With this definition it is easy to see that the universal property of the adjunction should hold, since we have
+where `-i` is the element of the
+[2-element type](univalent-combinatorics.2-element-types.md) obtained by
+applying the swap [involution](foundation.involutions.md) to `i`. With this
+definition it is easy to see that the universal property of the adjunction
+should hold, since we have
 
 ```text
   ((I,a) → S (I,a) → core R (I,a)) ≃ ((x y : A) → S {x,y} → R x y).

From 2fc1b239d9d3dc2ab5956db4e4fb72e0f25187c4 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 13 Sep 2023 14:52:40 +0200
Subject: [PATCH 18/23] rational monoids

---
 ...s-of-elements-commutative-monoids.lagda.md | 147 ++++++++++++++++--
 .../powers-of-elements-monoids.lagda.md       |   5 +-
 .../rational-commutative-monoids.lagda.md     |  72 ++++++++-
 3 files changed, 207 insertions(+), 17 deletions(-)

diff --git a/src/group-theory/powers-of-elements-commutative-monoids.lagda.md b/src/group-theory/powers-of-elements-commutative-monoids.lagda.md
index 4cd5d7bb08..56ffe733ca 100644
--- a/src/group-theory/powers-of-elements-commutative-monoids.lagda.md
+++ b/src/group-theory/powers-of-elements-commutative-monoids.lagda.md
@@ -7,30 +7,151 @@ module group-theory.powers-of-elements-commutative-monoids where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-natural-numbers
+open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
 
+open import foundation.identity-types
 open import foundation.universe-levels
 
 open import group-theory.commutative-monoids
+open import group-theory.homomorphisms-commutative-monoids
+open import group-theory.powers-of-elements-monoids
 ```
 
 </details>
 
-## Idea
-
-Consider an element `x` in a
-[commutative monoid](group-theory.commutative-monoids.md) and a
-[natural number](elementary-number-theory.natural-numbers.md) `n : ℕ`. The
-`n`-th **power** of `x` is the `n` times iterated product of `x` with itself.
+The **power operation** on a [monoid](group-theory.monoids.md) is the map
+`n x ↦ xⁿ`, which is defined by [iteratively](foundation.iterating-functions.md)
+multiplying `x` with itself `n` times.
 
 ## Definition
 
 ```agda
-power-Commutative-Monoid :
-  {l : Level} (M : Commutative-Monoid l) →
-  ℕ → type-Commutative-Monoid M → type-Commutative-Monoid M
-power-Commutative-Monoid M zero-ℕ x = unit-Commutative-Monoid M
-power-Commutative-Monoid M (succ-ℕ zero-ℕ) x = x
-power-Commutative-Monoid M (succ-ℕ (succ-ℕ n)) x =
-  mul-Commutative-Monoid M (power-Commutative-Monoid M (succ-ℕ n) x) x
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  power-Commutative-Monoid :
+    ℕ → type-Commutative-Monoid M → type-Commutative-Monoid M
+  power-Commutative-Monoid = power-Monoid (monoid-Commutative-Monoid M)
+```
+
+## Properties
+
+### `1ⁿ ＝ 1`
+
+```agda
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  power-unit-Commutative-Monoid :
+    (n : ℕ) →
+    power-Commutative-Monoid M n (unit-Commutative-Monoid M) ＝
+    unit-Commutative-Monoid M
+  power-unit-Commutative-Monoid zero-ℕ = refl
+  power-unit-Commutative-Monoid (succ-ℕ zero-ℕ) = refl
+  power-unit-Commutative-Monoid (succ-ℕ (succ-ℕ n)) =
+    right-unit-law-mul-Commutative-Monoid M _ ∙
+    power-unit-Commutative-Monoid (succ-ℕ n)
+```
+
+### `xⁿ⁺¹ = xⁿx`
+
+```agda
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  power-succ-Commutative-Monoid :
+    (n : ℕ) (x : type-Commutative-Monoid M) →
+    power-Commutative-Monoid M (succ-ℕ n) x ＝
+    mul-Commutative-Monoid M (power-Commutative-Monoid M n x) x
+  power-succ-Commutative-Monoid =
+    power-succ-Monoid (monoid-Commutative-Monoid M)
+```
+
+### `xⁿ⁺¹ ＝ xxⁿ`
+
+```agda
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  power-succ-Commutative-Monoid' :
+    (n : ℕ) (x : type-Commutative-Monoid M) →
+    power-Commutative-Monoid M (succ-ℕ n) x ＝
+    mul-Commutative-Monoid M x (power-Commutative-Monoid M n x)
+  power-succ-Commutative-Monoid' =
+    power-succ-Monoid' (monoid-Commutative-Monoid M)
+```
+
+### Powers by sums of natural numbers are products of powers
+
+```agda
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  distributive-power-add-Commutative-Monoid :
+    (m n : ℕ) {x : type-Commutative-Monoid M} →
+    power-Commutative-Monoid M (m +ℕ n) x ＝
+    mul-Commutative-Monoid M
+      ( power-Commutative-Monoid M m x)
+      ( power-Commutative-Monoid M n x)
+  distributive-power-add-Commutative-Monoid =
+    distributive-power-add-Monoid (monoid-Commutative-Monoid M)
+```
+
+### If `x` commutes with `y`, then powers distribute over the product of `x` and `y`
+
+```agda
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  distributive-power-mul-Commutative-Monoid :
+    (n : ℕ) {x y : type-Commutative-Monoid M} →
+    (H : mul-Commutative-Monoid M x y ＝ mul-Commutative-Monoid M y x) →
+    power-Commutative-Monoid M n (mul-Commutative-Monoid M x y) ＝
+    mul-Commutative-Monoid M
+      ( power-Commutative-Monoid M n x)
+      ( power-Commutative-Monoid M n y)
+  distributive-power-mul-Commutative-Monoid =
+    distributive-power-mul-Monoid (monoid-Commutative-Monoid M)
+```
+
+### Powers by products of natural numbers are iterated powers
+
+```agda
+module _
+  {l : Level} (M : Commutative-Monoid l)
+  where
+
+  power-mul-Commutative-Monoid :
+    (m n : ℕ) {x : type-Commutative-Monoid M} →
+    power-Commutative-Monoid M (m *ℕ n) x ＝
+    power-Commutative-Monoid M n (power-Commutative-Monoid M m x)
+  power-mul-Commutative-Monoid =
+    power-mul-Monoid (monoid-Commutative-Monoid M)
+```
+
+### Commutative-Monoid homomorphisms preserve powers
+
+```agda
+module _
+  {l1 l2 : Level} (M : Commutative-Monoid l1)
+  (N : Commutative-Monoid l2) (f : type-hom-Commutative-Monoid M N)
+  where
+
+  preserves-powers-hom-Commutative-Monoid :
+    (n : ℕ) (x : type-Commutative-Monoid M) →
+    map-hom-Commutative-Monoid M N f (power-Commutative-Monoid M n x) ＝
+    power-Commutative-Monoid N n (map-hom-Commutative-Monoid M N f x)
+  preserves-powers-hom-Commutative-Monoid =
+    preserves-powers-hom-Monoid
+      ( monoid-Commutative-Monoid M)
+      ( monoid-Commutative-Monoid N)
+      ( f)
 ```
diff --git a/src/group-theory/powers-of-elements-monoids.lagda.md b/src/group-theory/powers-of-elements-monoids.lagda.md
index 5e484a3e20..24b2cdd1d7 100644
--- a/src/group-theory/powers-of-elements-monoids.lagda.md
+++ b/src/group-theory/powers-of-elements-monoids.lagda.md
@@ -23,8 +23,9 @@ open import group-theory.monoids
 
 ## Idea
 
-The power operation on a monoid is the map `n x ↦ xⁿ`, which is defined by
-iteratively multiplying `x` with itself `n` times.
+The **power operation** on a [monoid](group-theory.monoids.md) is the map
+`n x ↦ xⁿ`, which is defined by [iteratively](foundation.iterating-functions.md)
+multiplying `x` with itself `n` times.
 
 ## Definition
 
diff --git a/src/group-theory/rational-commutative-monoids.lagda.md b/src/group-theory/rational-commutative-monoids.lagda.md
index 72417524c5..d21f79ca7a 100644
--- a/src/group-theory/rational-commutative-monoids.lagda.md
+++ b/src/group-theory/rational-commutative-monoids.lagda.md
@@ -9,10 +9,13 @@ module group-theory.rational-commutative-monoids where
 ```agda
 open import elementary-number-theory.natural-numbers
 
+open import foundation.dependent-pair-types
 open import foundation.equivalences
+open import foundation.identity-types
 open import foundation.universe-levels
 
 open import group-theory.commutative-monoids
+open import group-theory.monoids
 open import group-theory.powers-of-elements-commutative-monoids
 ```
 
@@ -24,9 +27,10 @@ A **rational commutative monoid** is a
 [commutative monoid](group-theory.commutative-monoids.md) `(M,0,+)` in which the
 map `x ↦ nx` is invertible for every natural number `n`.
 
-Note: since we usually write commutative monoids multiplicatively, the condition
+Note: Since we usually write commutative monoids multiplicatively, the condition
 that a commutative monoid is rational is that the map `x ↦ xⁿ` is invertible for
-every natural number `n`.
+every natural number `n`. However, for rational commutative monoids we will
+write the binary operation additively.
 
 ## Definition
 
@@ -36,4 +40,68 @@ every natural number `n`.
 is-rational-Commutative-Monoid : {l : Level} → Commutative-Monoid l → UU l
 is-rational-Commutative-Monoid M =
   (n : ℕ) → is-equiv (power-Commutative-Monoid M n)
+
+Rational-Commutative-Monoid : (l : Level) → UU (lsuc l)
+Rational-Commutative-Monoid l =
+  Σ (Commutative-Monoid l) is-rational-Commutative-Monoid
+
+module _
+  {l : Level} (M : Rational-Commutative-Monoid l)
+  where
+
+  commutative-monoid-Rational-Commutative-Monoid : Commutative-Monoid l
+  commutative-monoid-Rational-Commutative-Monoid = pr1 M
+
+  monoid-Rational-Commutative-Monoid : Monoid l
+  monoid-Rational-Commutative-Monoid =
+    monoid-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
+
+  type-Rational-Commutative-Monoid : UU l
+  type-Rational-Commutative-Monoid =
+    type-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
+
+  add-Rational-Commutative-Monoid :
+    (x y : type-Rational-Commutative-Monoid) →
+    type-Rational-Commutative-Monoid
+  add-Rational-Commutative-Monoid =
+    mul-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
+
+  zero-Rational-Commutative-Monoid : type-Rational-Commutative-Monoid
+  zero-Rational-Commutative-Monoid =
+    unit-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
+
+  associative-add-Rational-Commutative-Monoid :
+    (x y z : type-Rational-Commutative-Monoid) →
+    add-Rational-Commutative-Monoid
+      ( add-Rational-Commutative-Monoid x y)
+      ( z) ＝
+    add-Rational-Commutative-Monoid
+      ( x)
+      ( add-Rational-Commutative-Monoid y z)
+  associative-add-Rational-Commutative-Monoid =
+    associative-mul-Commutative-Monoid
+      commutative-monoid-Rational-Commutative-Monoid
+
+  left-unit-law-add-Rational-Commutative-Monoid :
+    (x : type-Rational-Commutative-Monoid) →
+    add-Rational-Commutative-Monoid zero-Rational-Commutative-Monoid x ＝ x
+  left-unit-law-add-Rational-Commutative-Monoid =
+    left-unit-law-mul-Commutative-Monoid
+      commutative-monoid-Rational-Commutative-Monoid
+
+  right-unit-law-add-Rational-Commutative-Monoid :
+    (x : type-Rational-Commutative-Monoid) →
+    add-Rational-Commutative-Monoid x zero-Rational-Commutative-Monoid ＝ x
+  right-unit-law-add-Rational-Commutative-Monoid =
+    right-unit-law-mul-Commutative-Monoid
+      commutative-monoid-Rational-Commutative-Monoid
+
+  multiple-Rational-Commutative-Monoid :
+    ℕ → type-Rational-Commutative-Monoid → type-Rational-Commutative-Monoid
+  multiple-Rational-Commutative-Monoid =
+    power-Commutative-Monoid commutative-monoid-Rational-Commutative-Monoid
+
+  is-rational-Rational-Commutative-Monoid :
+    (n : ℕ) → is-equiv (multiple-Rational-Commutative-Monoid n)
+  is-rational-Rational-Commutative-Monoid = pr2 M
 ```

From 834ca28a19840ab17461391472c4cdc35f3e76be Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 22 Oct 2023 19:07:14 +0200
Subject: [PATCH 19/23] remove --allow-unsolved-metas

---
 src/foundation/identity-systems.lagda.md | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/foundation/identity-systems.lagda.md b/src/foundation/identity-systems.lagda.md
index fbe2127062..e0c78d3023 100644
--- a/src/foundation/identity-systems.lagda.md
+++ b/src/foundation/identity-systems.lagda.md
@@ -1,8 +1,6 @@
 # Identity systems
 
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
-
 module foundation.identity-systems where
 ```
 

From ef8cc77f58759554929238d130dba82263303144 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 22 Oct 2023 19:08:47 +0200
Subject: [PATCH 20/23] undo undo changes

---
 src/foundation/symmetric-cores-binary-relations.lagda.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/foundation/symmetric-cores-binary-relations.lagda.md b/src/foundation/symmetric-cores-binary-relations.lagda.md
index 4ef3e91df9..4e06f7a76e 100644
--- a/src/foundation/symmetric-cores-binary-relations.lagda.md
+++ b/src/foundation/symmetric-cores-binary-relations.lagda.md
@@ -40,9 +40,9 @@ equipped with a counit
   (x y : A) → core R {x , y} → R x y
 ```
 
-that satisfyies the universal property of the symmetric core, i.e., it satisfies
-the property that for any symmetric relation `S : unordered-pair A → 𝒰` such
-that the precomposition function
+that satisfies the universal property of the symmetric core, i.e., it satisfies
+the property that for any symmetric relation `S : unordered-pair A → 𝒰`, the
+precomposition function
 
 ```text
   hom-Symmetric-Relation S (core R) → hom-Relation (rel S) R

From a8f7994a121b26ea3205de8dae5221dc415ca475 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 22 Oct 2023 19:10:03 +0200
Subject: [PATCH 21/23] remove incomplete changes

---
 .../symmetric-cores-binary-relations.lagda.md | 27 -------------------
 1 file changed, 27 deletions(-)

diff --git a/src/foundation/symmetric-cores-binary-relations.lagda.md b/src/foundation/symmetric-cores-binary-relations.lagda.md
index 4e06f7a76e..5d3d0b7c8d 100644
--- a/src/foundation/symmetric-cores-binary-relations.lagda.md
+++ b/src/foundation/symmetric-cores-binary-relations.lagda.md
@@ -105,33 +105,6 @@ module _
   map-universal-property-symmetric-core-Relation f x y s =
     counit-symmetric-core-Relation R (f (standard-unordered-pair x y) s)
 
-  map-inv-universal-property-symmetric-core-Relation :
-    hom-Relation (relation-Symmetric-Relation S) R →
-    hom-Symmetric-Relation S (symmetric-core-Relation R)
-  map-inv-universal-property-symmetric-core-Relation f p s i =
-    f ( element-unordered-pair p i)
-      ( other-element-unordered-pair p i)
-      ( tr-inv-Symmetric-Relation S
-        ( standard-unordered-pair
-          ( element-unordered-pair p i)
-          ( other-element-unordered-pair p i))
-        ( p)
-        ( compute-standard-unordered-pair-element-unordered-pair p i)
-        ( s))
-
-  is-section-map-inv-universal-property-symmetric-core-Relation :
-    map-universal-property-symmetric-core-Relation ∘
-    map-inv-universal-property-symmetric-core-Relation ~
-    id
-  is-section-map-inv-universal-property-symmetric-core-Relation f =
-    eq-htpy
-      ( λ p →
-        eq-htpy
-          ( λ s →
-            eq-htpy
-              ( λ i →
-                {!!})))
-
   equiv-universal-property-symmetric-core-Relation :
     hom-Symmetric-Relation S (symmetric-core-Relation R) ≃
     hom-Relation (relation-Symmetric-Relation S) R

From 2db8678604adc175b62c0b680a608a9bfa3f3a23 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 22 Oct 2023 19:11:33 +0200
Subject: [PATCH 22/23] fix imports

---
 src/foundation/symmetric-cores-binary-relations.lagda.md | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/foundation/symmetric-cores-binary-relations.lagda.md b/src/foundation/symmetric-cores-binary-relations.lagda.md
index 5d3d0b7c8d..e42c4546bd 100644
--- a/src/foundation/symmetric-cores-binary-relations.lagda.md
+++ b/src/foundation/symmetric-cores-binary-relations.lagda.md
@@ -10,8 +10,6 @@ module foundation.symmetric-cores-binary-relations where
 
 ```agda
 open import foundation.binary-relations
-open import foundation.function-extensionality
-open import foundation.function-types
 open import foundation.functoriality-dependent-function-types
 open import foundation.functoriality-function-types
 open import foundation.morphisms-binary-relations
@@ -22,7 +20,6 @@ open import foundation.universe-levels
 open import foundation.unordered-pairs
 
 open import foundation-core.equivalences
-open import foundation-core.homotopies
 
 open import univalent-combinatorics.standard-finite-types
 ```

From 3b65dcbf6ce9eeaed9e48b1ca305a171b1c70ff3 Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sun, 22 Oct 2023 19:12:17 +0200
Subject: [PATCH 23/23] remove --allow-unsolved-metas

---
 src/foundation/symmetric-operations.lagda.md | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/foundation/symmetric-operations.lagda.md b/src/foundation/symmetric-operations.lagda.md
index 5cbef9348e..2a2f8b4f5a 100644
--- a/src/foundation/symmetric-operations.lagda.md
+++ b/src/foundation/symmetric-operations.lagda.md
@@ -1,8 +1,6 @@
 # Symmetric operations
 
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
-
 module foundation.symmetric-operations where
 ```