From b2bd6bdfebdcdfe1a005c9dc7e1a26c430c3ea21 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 1 Jun 2023 21:34:40 -0700
Subject: [PATCH 01/19] def: refactor sum recursor

---
 src/Data/Sum/Base.lagda.md | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/src/Data/Sum/Base.lagda.md b/src/Data/Sum/Base.lagda.md
index dd21cf6fa..42efc3e6c 100644
--- a/src/Data/Sum/Base.lagda.md
+++ b/src/Data/Sum/Base.lagda.md
@@ -45,10 +45,26 @@ One of the most important things about sum types is the following property:
 given two functions `A → C` and `B → C`, we can construct a function
 `A ⊎ B → C`.
 
+<!--
+```agda
+⊎-elim
+  : ∀ {ℓ} (P : A ⊎ B → Type ℓ)
+  → (∀ (x : A) → P (inl x))
+  → (∀ (x : B) → P (inr x))
+  → (x : A ⊎ B) → P x
+⊎-elim P f g (inl x) = f x
+⊎-elim P f g (inr x) = g x
+```
+-->
+
 ```agda
+⊎-rec : (A → C) → (B → C) → (A ⊎ B) → C
+⊎-rec f g (inl x) = f x
+⊎-rec f g (inr x) = g x
+
 [_,_] : (A → C) → (B → C) → (A ⊎ B) → C
-[ f , g ] (inl x) = f x
-[ f , g ] (inr x) = g x
+[_,_] = ⊎-rec
+{-# INLINE [_,_] #-}
 ```
 
 Furthermore, this function is "universal" in the following sense: if we

From b601ec7282ce56a875d00bf1849d9686292d97bc Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 1 Jun 2023 21:34:57 -0700
Subject: [PATCH 02/19] wip: closure of relations

---
 src/Data/Rel/Closure.lagda.md | 273 ++++++++++++++++++++++++++++++++++
 1 file changed, 273 insertions(+)
 create mode 100644 src/Data/Rel/Closure.lagda.md

diff --git a/src/Data/Rel/Closure.lagda.md b/src/Data/Rel/Closure.lagda.md
new file mode 100644
index 000000000..bd6208521
--- /dev/null
+++ b/src/Data/Rel/Closure.lagda.md
@@ -0,0 +1,273 @@
+<!--
+```agda
+open import 1Lab.Prelude
+open import Data.Sum
+
+import Data.Nat as Nat
+import Data.Nat.Order as Nat
+```
+-->
+
+```agda
+module Data.Rel.Closure where
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  R S : A → A → Type ℓ
+```
+-->
+
+# Closures of relations
+
+A **closure operator** $-^{+}$ on relations takes a relation $R$ on a type
+$A$ to a new relation $R^{+}$ on $A$, where $R^{+}$ is the smallest
+relation containing $R$ that satisfies some property.
+
+<!-- [TODO: Reed M, 01/06/2023] Talk about monads here. -->
+
+## Reflexive Closure
+
+The reflexive closure of a relation $R$ is the smallest reflexive
+relation $R^{=}$ that contains $R$.
+
+```agda
+data Refl {A : Type ℓ} (R : A → A → Type ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where
+  reflexive : Refl R x x
+  [_] : ∀ {y} → R x y → Refl R x y
+  trunc : ∀ {y} → is-prop (Refl R x y)
+```
+
+<!--
+```agda
+instance
+  Refl-H-Level : ∀ {x y} {n} → H-Level (Refl R x y) (suc n)
+  Refl-H-Level = prop-instance trunc
+
+Refl-elim
+  : (P : ∀ (x y : A) → Refl R x y → Type ℓ'')
+  → (∀ {x y} → (r : R x y) → P x y [ r ])
+  → (∀ x → P x x reflexive)
+  → (∀ {x y} → (r+ : Refl R x y) → is-prop (P x y r+))
+  → ∀ {x y} → (r+ : Refl R x y) → P x y r+
+Refl-elim {R = R} P prel prefl pprop r+ = go r+ where
+  go : ∀ {x y} → (r+ : Refl R x y) → P x y r+
+  go reflexive = prefl _
+  go [ x ] = prel x
+  go (trunc r+ r+' i) =
+    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
+```
+-->
+
+The recursion principle for the reflexive closure of a relation witnesses
+the aforementioned universal property: it is the smallest reflexive
+relation containing $R$.
+
+```agda
+Refl-rec
+  : (S : A → A → Type ℓ)
+  → (∀ {x y} → R x y → S x y)
+  → (∀ x → S x x)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Refl R x y → S x y
+Refl-rec {R = R} S prel prefl pprop r+ = go r+ where
+  go : ∀ {x y} → Refl R x y → S x y
+  go reflexive = prefl _
+  go [ r ] = prel r
+  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
+```
+
+If the original relation is symmetric or transitive, then so is the
+reflexive closure.
+
+```agda
+refl-clo-symmetric
+  : (∀ {x y} → R x y → R y x)
+  → ∀ {x y} → Refl R x y → Refl R y x
+refl-clo-symmetric {R = R} is-sym =
+  Refl-rec (λ x y → Refl R y x)
+    (λ r → [ is-sym r ])
+    (λ _ → reflexive)
+    trunc
+
+refl-clo-transitive
+  : (∀ {x y z} → R x y → R y z → R x z)
+  → ∀ {x y z} → Refl R x y → Refl R y z → Refl R x z
+refl-clo-transitive is-trans reflexive s+ = s+
+refl-clo-transitive is-trans [ r ] reflexive = [ r ]
+refl-clo-transitive is-trans [ r ] [ s ] = [ is-trans r s ]
+refl-clo-transitive is-trans [ r ] (trunc s+ s+' i) =
+  trunc
+    (refl-clo-transitive is-trans [ r ] s+)
+    (refl-clo-transitive is-trans [ r ] s+') i
+refl-clo-transitive is-trans (trunc r+ r+' i) s+ =
+  trunc
+    (refl-clo-transitive is-trans r+ s+)
+    (refl-clo-transitive is-trans r+' s+) i
+```
+
+
+## Symmetric Closure
+
+The symmetric closure of a relation $R$ is the smallest reflexive
+relation $R^{\leftrightarrow}$ that contains $R$.
+
+```agda
+data Sym {A : Type ℓ} (R : A → A → Type ℓ') (x y : A) : Type (ℓ ⊔ ℓ') where
+  symmetric : R y x → Sym R x y
+  [_] : R x y → Sym R x y
+  trunc : is-prop (Sym R x y)
+```
+
+<!--
+```agda
+instance
+  Sym-H-Level : ∀ {x y} {n} → H-Level (Refl R x y) (suc n)
+  Sym-H-Level = prop-instance trunc
+
+Sym-elim
+  : (P : ∀ (x y : A) → Sym R x y → Type ℓ'')
+  → (∀ {x y} → (r : R x y) → P x y [ r ])
+  → (∀ {x y} → (r : R y x) → P x y (symmetric r))
+  → (∀ {x y} → (r+ : Sym R x y) → is-prop (P x y r+))
+  → ∀ {x y} → (r+ : Sym R x y) → P x y r+
+Sym-elim {R = R} P prel psym pprop r+ = go r+ where
+  go : ∀ {x y} → (r+ : Sym R x y) → P x y r+
+  go (symmetric x) = psym x
+  go [ x ] = prel x
+  go (trunc r+ r+' i) =
+    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
+```
+-->
+
+```agda
+Sym-rec
+  : (S : A → A → Type ℓ)
+  → (∀ {x y} → R x y → S x y)
+  → (∀ {x y} → R y x → S x y)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Sym R x y → S x y
+Sym-rec {R = R} S prel psym pprop r+ = go r+ where
+  go : ∀ {x y} → Sym R x y → S x y
+  go (symmetric r) = psym r
+  go [ r ] = prel r
+  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
+```
+
+If two elements $x$ and $y$ are related in the symmetric closure, then
+either $R x y$ or $R y x$ in the original relation.
+
+```agda
+sym-clo-rel
+  : ∀ {x y} → Sym R x y → ∥ (R x y) ⊎ (R y x) ∥
+sym-clo-rel {R = R} =
+  Sym-rec (λ x y → ∥ (R x y) ⊎ (R y x) ∥)
+    (λ r → inc (inl r))
+    (λ r → inc (inr r))
+    squash
+```
+
+
+
+If the original relation is reflexive, then so is the symmetric closure.
+
+```agda
+sym-clo-reflexive
+  : (∀ x → R x x)
+  → ∀ x → Sym R x x
+sym-clo-reflexive is-refl x = [ is-refl x ]
+```
+
+Note that this is *not* true for transitivity! To see why, consider an
+irreflexive transitive relation on a type with at least related 2
+elements $R x y$ . If the symmetric closure of this relation was
+transitive, we'd be able to create a loop $R^{\leftrightarrow} x x$ in
+the symmetric closure by composing the relations $R^{\leftrightarrow} x
+y$ and $R^{\leftrightarrow} y x$.  However, if two elements are related
+in the symmetric closure, then they must be related in the original
+relation, which leads directly to a contradiction, as the original
+relation is irreflexive.
+
+For simplicity, we show this for the strict ordering on the natural
+numbers.
+
+```agda
+private
+  ¬sym-clo-transitive
+    : ¬ (∀ {x y z} → Sym Nat._<_ x y → Sym Nat._<_ y z → Sym Nat._<_ x z)
+  ¬sym-clo-transitive sym-clo-trans =
+    ∥-∥-rec! (⊎-rec (Nat.<-irrefl refl) (Nat.<-irrefl refl))
+      (sym-clo-rel (sym-clo-trans [ 0<1 ] (symmetric 0<1)))
+    where
+      0<1 : 0 Nat.< 1
+      0<1 = Nat.s≤s Nat.0≤x
+```
+
+
+## Transitive Closure
+
+```agda
+data Trans {A : Type ℓ} (_~_ : A → A → Type ℓ') (x z : A) : Type (ℓ ⊔ ℓ') where
+  [_] : x ~ z → Trans _~_ x z
+  transitive : ∀ {y} → Trans _~_ x y → Trans _~_ y z → Trans _~_ x z
+  trunc : is-prop (Trans _~_ x z)
+```
+
+<!--
+```agda
+instance
+  Trans-H-Level : ∀ {x y} {n} → H-Level (Trans R x y) (suc n)
+  Trans-H-Level = prop-instance trunc
+```
+-->
+
+```agda
+Trans-elim
+  : (P : ∀ (x y : A) → Trans R x y → Type ℓ'')
+  → (∀ {x y} → (r : R x y) → P x y [ r ])
+  → (∀ {x y z} → (r+ : Trans R x y) → (s+ : Trans R y z)
+     → P x y r+ → P y z s+
+     → P x z (transitive r+ s+))
+  → (∀ {x y} → (r+ : Trans R x y) → is-prop (P x y r+))
+  → ∀ {x y} → (r+ : Trans R x y) → P x y r+
+Trans-elim {R = R} P prel ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → (r+ : Trans R x y) → P x y r+
+  go [ r ] = prel r
+  go (transitive r+ s+) = ptrans r+ s+ (go r+) (go s+)
+  go (trunc r+ r+' i) =
+    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
+
+Trans-rec
+  : (∀ {x y} → (r : R x y) → X)
+  → (X → X → X)
+  → is-prop X
+  → ∀ {x y} → Trans R x y → X
+Trans-rec {R = R} {X = X} prel ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → Trans R x y → X
+  go [ r ] = prel r
+  go (transitive r+ s+) = ptrans (go r+) (go s+)
+  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
+```
+
+If the original relation is reflexive or symmetric, then so is the
+transitive closure.
+
+```agda
+trans-clo-reflexive
+  : (∀ x → R x x)
+  → ∀ x → Trans R x x
+trans-clo-reflexive is-refl x = [ is-refl x ]
+
+trans-clo-symmetric
+  : (∀ {x y} → R x y → R y x)
+  → ∀ {x y} → Trans R x y → Trans R y x
+trans-clo-symmetric is-sym [ r ] =
+  [ is-sym r ]
+trans-clo-symmetric is-sym (transitive r+ r+') =
+  transitive (trans-clo-symmetric is-sym r+') (trans-clo-symmetric is-sym r+)
+trans-clo-symmetric is-sym (trunc r+ r+' i) =
+  trunc (trans-clo-symmetric is-sym r+) (trans-clo-symmetric is-sym r+') i
+```

From 48adc16e4b81e182efcf4aadf802f2586ad4e499 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 1 Jun 2023 22:05:47 -0700
Subject: [PATCH 03/19] wip: more closures

---
 src/Data/Rel/Closure.lagda.md | 119 +++++++++++++++++++++++++++++-----
 1 file changed, 102 insertions(+), 17 deletions(-)

diff --git a/src/Data/Rel/Closure.lagda.md b/src/Data/Rel/Closure.lagda.md
index bd6208521..85b0b03f1 100644
--- a/src/Data/Rel/Closure.lagda.md
+++ b/src/Data/Rel/Closure.lagda.md
@@ -112,7 +112,7 @@ refl-clo-transitive is-trans (trunc r+ r+' i) s+ =
 
 ## Symmetric Closure
 
-The symmetric closure of a relation $R$ is the smallest reflexive
+The symmetric closure of a relation $R$ is the smallest symmetric
 relation $R^{\leftrightarrow}$ that contains $R$.
 
 ```agda
@@ -143,6 +143,10 @@ Sym-elim {R = R} P prel psym pprop r+ = go r+ where
 ```
 -->
 
+Like the reflexive closure, the recursion principle for the symmetric
+closure witnesses it's universal property; it is the smallest symmetric
+relation containing $R$.
+
 ```agda
 Sym-rec
   : (S : A → A → Type ℓ)
@@ -209,6 +213,9 @@ private
 
 ## Transitive Closure
 
+The transitive closure of a relation $R$ is the smallest transitive
+relation $R^{+}$ that contains $R$.
+
 ```agda
 data Trans {A : Type ℓ} (_~_ : A → A → Type ℓ') (x z : A) : Type (ℓ ⊔ ℓ') where
   [_] : x ~ z → Trans _~_ x z
@@ -221,12 +228,9 @@ data Trans {A : Type ℓ} (_~_ : A → A → Type ℓ') (x z : A) : Type (ℓ 
 instance
   Trans-H-Level : ∀ {x y} {n} → H-Level (Trans R x y) (suc n)
   Trans-H-Level = prop-instance trunc
-```
--->
 
-```agda
 Trans-elim
-  : (P : ∀ (x y : A) → Trans R x y → Type ℓ'')
+  : (P : ∀ (x y : A) → Trans R x y → Type ℓ)
   → (∀ {x y} → (r : R x y) → P x y [ r ])
   → (∀ {x y z} → (r+ : Trans R x y) → (s+ : Trans R y z)
      → P x y r+ → P y z s+
@@ -239,14 +243,21 @@ Trans-elim {R = R} P prel ptrans pprop r+ = go r+ where
   go (transitive r+ s+) = ptrans r+ s+ (go r+) (go s+)
   go (trunc r+ r+' i) =
     is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
+```
+-->
+
+The recursion principle for the transitive closure witnesses it's
+universal property; it is the smallest transitive relation containing $R$.
 
+```agda
 Trans-rec
-  : (∀ {x y} → (r : R x y) → X)
-  → (X → X → X)
-  → is-prop X
-  → ∀ {x y} → Trans R x y → X
-Trans-rec {R = R} {X = X} prel ptrans pprop r+ = go r+ where
-  go : ∀ {x y} → Trans R x y → X
+  : (S : A → A → Type ℓ)
+  → (∀ {x y} → (r : R x y) → S x y)
+  → (∀ {x y z} → S x y → S y z → S x z)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Trans R x y → S x y
+Trans-rec {R = R} S prel ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → Trans R x y → S x y
   go [ r ] = prel r
   go (transitive r+ s+) = ptrans (go r+) (go s+)
   go (trunc r+ r+' i) = pprop (go r+) (go r+') i
@@ -264,10 +275,84 @@ trans-clo-reflexive is-refl x = [ is-refl x ]
 trans-clo-symmetric
   : (∀ {x y} → R x y → R y x)
   → ∀ {x y} → Trans R x y → Trans R y x
-trans-clo-symmetric is-sym [ r ] =
-  [ is-sym r ]
-trans-clo-symmetric is-sym (transitive r+ r+') =
-  transitive (trans-clo-symmetric is-sym r+') (trans-clo-symmetric is-sym r+)
-trans-clo-symmetric is-sym (trunc r+ r+' i) =
-  trunc (trans-clo-symmetric is-sym r+) (trans-clo-symmetric is-sym r+') i
+trans-clo-symmetric {R = R} is-sym r+ =
+  Trans-rec (λ x y → Trans R y x)
+    (λ r → [ is-sym r ])
+    (λ r+ s+ → transitive s+ r+)
+    trunc
+    r+
+```
+
+## Reflexive-Transitive Closure
+
+The transitive closure of a relation $R$ is the smallest reflexive and
+transitive relation $R^{*}$ that contains $R$.
+
+```agda
+data Refl-trans {A : Type ℓ} (R : A → A → Type ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where
+  [_] : ∀ {y} → R x y → Refl-trans R x y
+  reflexive : Refl-trans R x x
+  transitive : ∀ {y z} → Refl-trans R x y → Refl-trans R y z → Refl-trans R x z
+  trunc : ∀ {y} → is-prop (Refl-trans R x y)
+```
+
+<!--
+```agda
+instance
+  Refl-trans-H-Level : ∀ {x y} {n} → H-Level (Trans R x y) (suc n)
+  Refl-trans-H-Level = prop-instance trunc
+
+Refl-trans-elim
+  : (P : ∀ (x y : A) → Refl-trans R x y → Type ℓ'')
+  → (∀ {x y} → (r : R x y) → P x y [ r ])
+  → (∀ {x} → P x x reflexive)
+  → (∀ {x y z} → (r+ : Refl-trans R x y) → (s+ : Refl-trans R y z)
+     → P x y r+ → P y z s+
+     → P x z (transitive r+ s+))
+  → (∀ {x y} → (r+ : Refl-trans R x y) → is-prop (P x y r+))
+  → ∀ {x y} → (r+ : Refl-trans R x y) → P x y r+
+Refl-trans-elim {R = R} P prel prefl ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → (r+ : Refl-trans R x y) → P x y r+
+  go [ r ] = prel r
+  go reflexive = prefl
+  go (transitive r+ s+) = ptrans r+ s+ (go r+) (go s+)
+  go (trunc r+ r+' i) =
+    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
+```
+-->
+
+Following the general theme, the recursion principle for the reflexive
+transitive closure witnesses it's universal property; it is the smallest
+transitive relation containing $R$.
+
+```agda
+Refl-trans-rec
+  : (S : A → A → Type ℓ)
+  → (∀ {x y} → (r : R x y) → S x y)
+  → (∀ {x} → S x x)
+  → (∀ {x y z} → S x y → S y z → S x z)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Refl-trans R x y → S x y
+Refl-trans-rec {R = R} S prel prefl ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → Refl-trans R x y → S x y
+  go [ r ] = prel r
+  go reflexive = prefl
+  go (transitive r+ s+) = ptrans (go r+) (go s+)
+  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
+```
+
+If the underlying relation is symmetric, then so is the
+reflexive-transitive closure.
+
+```agda
+refl-trans-clo-symmetric
+  : (∀ {x y} → R x y → R y x)
+  → ∀ {x y} → Refl-trans R x y → Refl-trans R y x
+refl-trans-clo-symmetric {R = R} is-sym r+ =
+  Refl-trans-rec (λ x y → Refl-trans R y x)
+    (λ r → [ is-sym r ])
+    reflexive
+    (λ r+ s+ → transitive s+ r+)
+    trunc
+    r+
 ```

From b5f5e082ba1416feabbdec2f4c79d2a7c7c8812d Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 1 Jun 2023 23:12:48 -0700
Subject: [PATCH 04/19] wip: modify some recursion principles

---
 src/Data/Rel/Closure.lagda.md | 112 ++++++++++++++++++++++++++++++++--
 1 file changed, 107 insertions(+), 5 deletions(-)

diff --git a/src/Data/Rel/Closure.lagda.md b/src/Data/Rel/Closure.lagda.md
index 85b0b03f1..ea42757c8 100644
--- a/src/Data/Rel/Closure.lagda.md
+++ b/src/Data/Rel/Closure.lagda.md
@@ -151,7 +151,7 @@ relation containing $R$.
 Sym-rec
   : (S : A → A → Type ℓ)
   → (∀ {x y} → R x y → S x y)
-  → (∀ {x y} → R y x → S x y)
+  → (∀ {x y} → R x y → S y x)
   → (∀ {x y} → is-prop (S x y))
   → ∀ {x y} → Sym R x y → S x y
 Sym-rec {R = R} S prel psym pprop r+ = go r+ where
@@ -285,8 +285,8 @@ trans-clo-symmetric {R = R} is-sym r+ =
 
 ## Reflexive-Transitive Closure
 
-The transitive closure of a relation $R$ is the smallest reflexive and
-transitive relation $R^{*}$ that contains $R$.
+The reflexive-transitive closure of a relation $R$ is the smallest
+reflexive and transitive relation $R^{*}$ that contains $R$.
 
 ```agda
 data Refl-trans {A : Type ℓ} (R : A → A → Type ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where
@@ -299,7 +299,7 @@ data Refl-trans {A : Type ℓ} (R : A → A → Type ℓ') (x : A) : A → Type
 <!--
 ```agda
 instance
-  Refl-trans-H-Level : ∀ {x y} {n} → H-Level (Trans R x y) (suc n)
+  Refl-trans-H-Level : ∀ {x y} {n} → H-Level (Refl-trans R x y) (suc n)
   Refl-trans-H-Level = prop-instance trunc
 
 Refl-trans-elim
@@ -323,7 +323,7 @@ Refl-trans-elim {R = R} P prel prefl ptrans pprop r+ = go r+ where
 
 Following the general theme, the recursion principle for the reflexive
 transitive closure witnesses it's universal property; it is the smallest
-transitive relation containing $R$.
+reflexive and transitive relation containing $R$.
 
 ```agda
 Refl-trans-rec
@@ -356,3 +356,105 @@ refl-trans-clo-symmetric {R = R} is-sym r+ =
     trunc
     r+
 ```
+
+## Reflexive-Symmetric-Transitive Closure
+
+Finally, the reflexive-symmetric-transitive closure of a relation $R$ is
+the smallest reflexive, symmetric, and transitive relation
+$R^{\leftrightarrow*}$ that contains $R$.
+
+```agda
+data Refl-sym-trans {A : Type ℓ} (R : A → A → Type ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where
+  [_] : ∀ {y} → R x y → Refl-sym-trans R x y
+  reflexive : Refl-sym-trans R x x
+  symmetric : ∀ {y} → Refl-sym-trans R y x → Refl-sym-trans R x y
+  transitive : ∀ {y z} → Refl-sym-trans R x y → Refl-sym-trans R y z → Refl-sym-trans R x z
+  trunc : ∀ {y} → is-prop (Refl-sym-trans R x y)
+```
+
+<!--
+```agda
+instance
+  Refl-sym-trans-H-Level : ∀ {x y} {n} → H-Level (Refl-sym-trans R x y) (suc n)
+  Refl-sym-trans-H-Level = prop-instance trunc
+
+Refl-sym-trans-elim
+  : (P : ∀ (x y : A) → Refl-sym-trans R x y → Type ℓ'')
+  → (∀ {x y} → (r : R x y) → P x y [ r ])
+  → (∀ {x} → P x x reflexive)
+  → (∀ {x y} → (r+ : Refl-sym-trans R x y)
+     → P x y r+ → P y x (symmetric r+))
+  → (∀ {x y z} → (r+ : Refl-sym-trans R x y) → (s+ : Refl-sym-trans R y z)
+     → P x y r+ → P y z s+
+     → P x z (transitive r+ s+))
+  → (∀ {x y} → (r+ : Refl-sym-trans R x y) → is-prop (P x y r+))
+  → ∀ {x y} → (r+ : Refl-sym-trans R x y) → P x y r+
+Refl-sym-trans-elim {R = R} P prel prefl psym ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → (r+ : Refl-sym-trans R x y) → P x y r+
+  go [ r ] = prel r
+  go reflexive = prefl
+  go (symmetric r) = psym r (go r)
+  go (transitive r+ s+) = ptrans r+ s+ (go r+) (go s+)
+  go (trunc r+ r+' i) =
+    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
+```
+-->
+
+Yet again, the recursion principle for the reflexive, symmetric,
+transitive closure witnesses it's universal property; it is the smallest
+reflexive, symmetric, transitive relation containing $R$.
+
+```agda
+Refl-sym-trans-rec
+  : (S : A → A → Type ℓ)
+  → (∀ {x y} → (r : R x y) → S x y)
+  → (∀ {x} → S x x)
+  → (∀ {x y} → S x y → S y x)
+  → (∀ {x y z} → S x y → S y z → S x z)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Refl-sym-trans R x y → S x y
+Refl-sym-trans-rec {R = R} S prel prefl psym ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → Refl-sym-trans R x y → S x y
+  go [ r ] = prel r
+  go reflexive = prefl
+  go (symmetric r) = psym (go r)
+  go (transitive r+ s+) = ptrans (go r+) (go s+)
+  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
+```
+
+We also define an alternative recursion principle for inducting down
+the length of the chain of relations.
+
+```agda
+Refl-sym-trans-rec-length
+  : (S : A → A → Type ℓ)
+  → (∀ {x} → S x x)
+  → (∀ {x y z} → R x y → S y z → S x z)
+  → (∀ {x y z} → R y x → S y z → S x z)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Refl-sym-trans R x y → S x y
+Refl-sym-trans-rec-length {R = R} S pnil pstep pinv pprop r+ = go r+ pnil where
+  go : ∀ {x y z} → Refl-sym-trans R x y → S y z → S x z
+  go-sym : ∀ {x y z} → Refl-sym-trans R y x → S y z → S x z
+
+  go [ r ] acc = pstep r acc
+  go reflexive acc = acc
+  go (symmetric r+) acc = go-sym r+ acc
+  go (transitive r+ s+) acc = go r+ (go s+ acc)
+  go (trunc r+ r+' i) acc = pprop (go r+ acc) (go r+' acc) i
+
+  go-sym [ r ] acc = pinv r acc
+  go-sym reflexive acc = acc
+  go-sym (symmetric r+) acc = go r+ acc
+  go-sym (transitive r+ s+) acc = go-sym s+ (go-sym r+ acc)
+  go-sym (trunc r+ r+' i) acc = pprop (go-sym r+ acc) (go-sym r+' acc) i
+```
+
+We
+
+```agda
+refl-trans→refl-sym-trans
+  : ∀ {x y} → Refl-trans R x y → Refl-sym-trans R x y
+refl-trans→refl-sym-trans =
+  Refl-trans-rec (Refl-sym-trans _) [_] reflexive transitive trunc
+```

From 5e6453f00e18892051368fe55fcfd91556e8c054 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 1 Jun 2023 23:13:04 -0700
Subject: [PATCH 05/19] wip: church rosser = confluence = semiconfluence

---
 src/Data/Rel/Confluent.lagda.md | 77 +++++++++++++++++++++++++++++++++
 1 file changed, 77 insertions(+)
 create mode 100644 src/Data/Rel/Confluent.lagda.md

diff --git a/src/Data/Rel/Confluent.lagda.md b/src/Data/Rel/Confluent.lagda.md
new file mode 100644
index 000000000..6c715da01
--- /dev/null
+++ b/src/Data/Rel/Confluent.lagda.md
@@ -0,0 +1,77 @@
+<!--
+```agda
+open import 1Lab.Prelude
+
+open import Data.Rel.Closure
+```
+-->
+
+```agda
+module Data.Rel.Confluent where
+```
+
+# Confluence
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  R : A → A → Type ℓ
+```
+-->
+
+```agda
+has-church-rosser : (A → A → Type ℓ) → Type _
+has-church-rosser {A = A} R =
+  ∀ {x y} → Refl-sym-trans R x y
+  → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z)
+
+is-confluent : (A → A → Type ℓ) → Type _
+is-confluent {A = A} R =
+  ∀ {a x y} → Refl-trans R a x → Refl-trans R a y
+  → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z)
+
+is-semi-confluent : (A → A → Type ℓ) → Type _
+is-semi-confluent {A = A} R =
+  ∀ {a x y} → Refl-trans R a x → R a y
+  → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z)
+
+church-rosser→confluent : has-church-rosser R → is-confluent R
+church-rosser→confluent church-rosser r+ s+ =
+  church-rosser $
+    transitive
+      (symmetric (refl-trans→refl-sym-trans r+))
+      (refl-trans→refl-sym-trans s+)
+
+semiconfluent→church-rosser : is-semi-confluent R → has-church-rosser R
+semiconfluent→church-rosser {R = R} semiconf r+ =
+  Refl-sym-trans-rec-length
+    (λ x y →  ∃[ z ∈ _ ] (Refl-trans R x z × Refl-trans R y z))
+    (inc (_ , reflexive , reflexive))
+    (λ x~y r+ → do
+      z' , y~z' , z~z' ← r+
+      z'' , z'~z'' , y~z'' ← semiconf (transitive [ x~y ] y~z') x~y
+      pure (z'' , transitive [ x~y ] y~z'' , transitive z~z' z'~z''))
+    (λ y~x r+ → do
+      z' , y~z' , z~z' ← r+
+      z'' , z'~z'' , x~z'' ← semiconf y~z' y~x
+      pure (z'' , x~z'' , transitive z~z' z'~z''))
+    squash
+    r+
+
+confluent→semiconfluent : is-confluent R → is-semi-confluent R
+confluent→semiconfluent conf r+ s = conf r+ [ s ]
+
+semiconfluent→confluent : is-semi-confluent R → is-confluent R
+semiconfluent→confluent conf =
+  church-rosser→confluent (semiconfluent→church-rosser conf)
+
+confluent→church-rosser : is-confluent R → has-church-rosser R
+confluent→church-rosser conf =
+  semiconfluent→church-rosser (confluent→semiconfluent conf)
+
+church-rosser→semiconfluent : has-church-rosser R → is-semi-confluent R
+church-rosser→semiconfluent church-rosser =
+  confluent→semiconfluent (church-rosser→confluent church-rosser)
+```

From a0f50fe17aac6cd93787feb35d3e720692fda9f3 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Fri, 2 Jun 2023 16:53:38 -0700
Subject: [PATCH 06/19] def: confluence, strong normalisation

---
 src/Data/Rel/Closure.lagda.md              |  90 +++-
 src/Rewriting/Confluent.lagda.md           | 515 +++++++++++++++++++++
 src/Rewriting/StronglyNormalising.lagda.md |  82 ++++
 3 files changed, 668 insertions(+), 19 deletions(-)
 create mode 100644 src/Rewriting/Confluent.lagda.md
 create mode 100644 src/Rewriting/StronglyNormalising.lagda.md

diff --git a/src/Data/Rel/Closure.lagda.md b/src/Data/Rel/Closure.lagda.md
index ea42757c8..4ab7a7a08 100644
--- a/src/Data/Rel/Closure.lagda.md
+++ b/src/Data/Rel/Closure.lagda.md
@@ -341,6 +341,53 @@ Refl-trans-rec {R = R} S prel prefl ptrans pprop r+ = go r+ where
   go (trunc r+ r+' i) = pprop (go r+) (go r+') i
 ```
 
+We also provide a recursion principle that inducts down the length of the
+chain of relations.
+
+```agda
+Refl-trans-rec-chain
+  : (S : A → A → Type ℓ)
+  → (∀ {x} → S x x)
+  → (∀ {x y z} → R x y → Refl-trans R y z → S y z → S x z)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Refl-trans R x y → S x y
+Refl-trans-rec-chain {R = R} S pnil pstep pprop r+ = go r+ reflexive pnil where
+  go : ∀ {x y z} → Refl-trans R x y → Refl-trans R y z → S y z → S x z
+  go [ x→y ] y→*z acc = pstep x→y y→*z acc
+  go reflexive y→*z acc = acc
+  go (transitive x→*x' x'→*y) y→*z acc =
+    go x→*x' (transitive x'→*y y→*z) (go x'→*y y→*z acc)
+  go (trunc x→*y x→*y' i) y→*z acc =
+    pprop (go x→*y y→*z acc) (go x→*y' y→*z acc) i
+```
+
+We also provide an eliminator for inspecting forks.
+
+```agda
+Refl-trans-case-fork
+  : (S : A → A → A → Type ℓ)
+  → (∀ {a y} → Refl-trans R a y → S a a y)
+  → (∀ {a x} → Refl-trans R a x → S a x a)
+  → (∀ {a x y x' y'}
+     → R a x' → Refl-trans R x' x
+     → R a y' → Refl-trans R y' y
+     → S a x y)
+  → (∀ {a x y} → is-prop (S a x y))
+  → ∀ {a x y} → Refl-trans R a x → Refl-trans R a y → S a x y
+Refl-trans-case-fork {R = R} S refll reflr fork prop {a} {x} {y} a→*x a→*y =
+  Refl-trans-rec-chain (λ a x → Refl-trans R a y → S a x y)
+    refll
+    (λ {a} {a'} {x} a→a' a'→*x _ a→*y →
+      Refl-trans-rec-chain
+        (λ a y → R a a' → Refl-trans R a' x → S a x y)
+        (λ a→a' a'→*x → reflr (transitive [ a→a' ] a'→*x))
+        (λ a→a' a'→*y _ a→a'' a''→*x → fork a→a'' a''→*x a→a' a'→*y)
+        (Π-is-hlevel 1 (λ _ → Π-is-hlevel 1 λ _ → prop))
+        a→*y a→a' a'→*x)
+    (Π-is-hlevel 1 (λ _ → prop))
+    a→*x a→*y
+```
+
 If the underlying relation is symmetric, then so is the
 reflexive-transitive closure.
 
@@ -426,31 +473,36 @@ We also define an alternative recursion principle for inducting down
 the length of the chain of relations.
 
 ```agda
-Refl-sym-trans-rec-length
+Refl-sym-trans-rec-chain
   : (S : A → A → Type ℓ)
   → (∀ {x} → S x x)
-  → (∀ {x y z} → R x y → S y z → S x z)
-  → (∀ {x y z} → R y x → S y z → S x z)
+  → (∀ {x y z} → R x y → Refl-sym-trans R y z → S y z → S x z)
+  → (∀ {x y z} → R y x → Refl-sym-trans R y z → S y z → S x z)
   → (∀ {x y} → is-prop (S x y))
   → ∀ {x y} → Refl-sym-trans R x y → S x y
-Refl-sym-trans-rec-length {R = R} S pnil pstep pinv pprop r+ = go r+ pnil where
-  go : ∀ {x y z} → Refl-sym-trans R x y → S y z → S x z
-  go-sym : ∀ {x y z} → Refl-sym-trans R y x → S y z → S x z
-
-  go [ r ] acc = pstep r acc
-  go reflexive acc = acc
-  go (symmetric r+) acc = go-sym r+ acc
-  go (transitive r+ s+) acc = go r+ (go s+ acc)
-  go (trunc r+ r+' i) acc = pprop (go r+ acc) (go r+' acc) i
-
-  go-sym [ r ] acc = pinv r acc
-  go-sym reflexive acc = acc
-  go-sym (symmetric r+) acc = go r+ acc
-  go-sym (transitive r+ s+) acc = go-sym s+ (go-sym r+ acc)
-  go-sym (trunc r+ r+' i) acc = pprop (go-sym r+ acc) (go-sym r+' acc) i
+Refl-sym-trans-rec-chain {R = R} S pnil pstep pinv pprop r+ = go r+ reflexive pnil where
+  go : ∀ {x y z} → Refl-sym-trans R x y → Refl-sym-trans R y z → S y z → S x z
+  go-sym : ∀ {x y z} → Refl-sym-trans R y x → Refl-sym-trans R y z → S y z → S x z
+
+  go [ x→y ] y→*z acc = pstep x→y y→*z acc
+  go reflexive y→*z acc = acc
+  go (symmetric y→*x) y→*z acc = go-sym y→*x y→*z acc
+  go (transitive x→*x' x'→*y) y→*z acc =
+    go x→*x' (transitive x'→*y y→*z) (go x'→*y y→*z acc)
+  go (trunc x→*y x→*y' i) y→*z acc =
+    pprop (go x→*y y→*z acc) (go x→*y' y→*z acc) i
+
+  go-sym [ y→x ] y→*z acc = pinv y→x y→*z acc
+  go-sym reflexive y→*z acc = acc
+  go-sym (symmetric x→*y) y→*z acc = go x→*y y→*z acc
+  go-sym (transitive y→*y' y'→*x) y→*z acc =
+    go-sym y'→*x (transitive (symmetric y→*y') y→*z) (go-sym y→*y' y→*z acc)
+  go-sym (trunc y→*x y→*x' i) y→*z acc =
+    pprop (go-sym y→*x y→*z acc) (go-sym y→*x' y→*z acc) i
 ```
 
-We
+The reflexive-transitive closure embeds into the reflexive symmetric
+transitive closure.
 
 ```agda
 refl-trans→refl-sym-trans
diff --git a/src/Rewriting/Confluent.lagda.md b/src/Rewriting/Confluent.lagda.md
new file mode 100644
index 000000000..08160c1b3
--- /dev/null
+++ b/src/Rewriting/Confluent.lagda.md
@@ -0,0 +1,515 @@
+```agda
+open import Rewriting.StronglyNormalising
+
+open import 1Lab.Prelude
+
+open import Data.Rel.Closure
+open import Data.Wellfounded.Base
+```
+-->
+
+```agda
+module Rewriting.Confluent where
+```
+
+# Confluent Rewriting Systems
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  R : A → A → Type ℓ
+```
+-->
+
+Many problems in computer science can be phrased in terms of
+**term rewriting systems**. Concretely, these are given by a collection
+of terms in some language, along with a collection of rules that describe
+how we can simplify terms. As an example, the untyped $\lambda$-calculus
+can be naturally presented as a term rewriting system, where only
+reduction rule is $\beta$-reduction. More abstractly, a rewriting system
+on a type $A$ is simply a relation $\leadsto$ on $A$ which encodes the
+rewriting rules. Sequences of rewrites are then described using the
+[reflexive transitive closure] of $\leadsto$.
+
+[reflexive transitive closure]: Data.Rel.Closure.html#reflexive-transitive-closure.html
+
+Note that term rewriting systems may be non-deterministic, as multiple
+rewrite rules can apply to a term $t$. This means that multiple
+strategies of applying the rules may lead to different answers, which is
+quite problematic if we want to use the rewriting system to simplify
+expressions. It would be useful if we could prove *some* property of the
+relation that would guarantee that this situation does not occur.
+
+This leads us to the notion of **confluence**. We say a relation $\leadsto$
+is confluent if there for all pairs of reduction chains $a \leadsto^{*} x$
+and $a \leadsto^{*} y$, there exists some $z$ such that $x \leadsto^{*} z$
+and $y \leadsto^{*} z$, as in the following diagram.
+
+~~~{.quiver}
+\begin{tikzcd}
+  a && y \\
+  \\
+  x && {\exists z}
+  \arrow["{*}"', from=1-1, to=3-1]
+  \arrow["{*}"', dashed, from=3-1, to=3-3]
+  \arrow["{*}", dashed, from=1-3, to=3-3]
+  \arrow["{*}", from=1-1, to=1-3]
+\end{tikzcd}
+~~~
+
+```agda
+is-confluent : (A → A → Type ℓ) → Type _
+is-confluent {A = A} R =
+  ∀ {a x y} → Refl-trans R a x → Refl-trans R a y
+  → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z)
+```
+
+Note that this does *not* mean that all rewriting sequences terminate
+regardless of strategy. For instance, consider the following rewriting
+system:
+
+~~~{.quiver}
+\begin{tikzcd}
+  \bullet & \bullet & \bullet & \cdots \\
+  \\
+  \bullet
+  \arrow[from=1-1, to=3-1]
+  \arrow[from=1-2, to=3-1]
+  \arrow[from=1-3, to=3-1]
+  \arrow[from=1-2, to=1-3]
+  \arrow[from=1-1, to=1-2]
+  \arrow[from=1-4, to=3-1]
+  \arrow[from=1-3, to=1-4]
+\end{tikzcd}
+~~~
+
+There is an infinitely long sequence of rewrites extending to the right,
+so a bad strategy will never terminate. However, we can always reconcile
+diverging paths by rewriting to the term at the bottom of the diagram.
+
+<!-- [TODO: Reed M, 02/06/2023] Prove this using Maybe (Nat ^op) -->
+
+## The Church-Rosser Property
+
+A rewriting system $\leadsto$ yields an equivalence relation on terms via
+the [reflexive symmetric transitive closure] of $\leadsto$. This leads to
+a variant of confluence known as the **Church-Rosser Property**, which
+requires a $z$ for every pair of equivalent terms $x$ and $y$ such that
+$x \leadsto^{z}$ and $y \leadsto^{z}$.
+
+[reflexive symmetric transitive closure]: Data.Rel.Closure.html#reflexive-symmetric-transitive-closure.html
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && y \\
+  & z
+  \arrow["{*}"', dashed, from=1-1, to=2-2]
+  \arrow["{*}", dashed, from=1-3, to=2-2]
+  \arrow["{*}", tail reversed, from=1-1, to=1-3]
+\end{tikzcd}
+~~~
+
+```agda
+has-church-rosser : (A → A → Type ℓ) → Type _
+has-church-rosser {A = A} R =
+  ∀ {x y} → Refl-sym-trans R x y
+  → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z)
+```
+
+At first glance, this seems like a stronger condition than confluence,
+as Church-Rosser also gives us diamonds of the following shape:
+
+~~~{.quiver}
+\begin{tikzcd}
+  a && y \\
+  \\
+  x && {\exists z}
+  \arrow["{*}", from=3-1, to=1-1]
+  \arrow["{*}"', dashed, from=3-1, to=3-3]
+  \arrow["{*}", dashed, from=1-3, to=3-3]
+  \arrow["{*}"', from=1-3, to=1-1]
+\end{tikzcd}
+~~~
+
+Somewhat surprisingly, it turns out that the two conditions are equivalent!
+Showing that Church-Rosser implies confluence is rather easy: if we
+have two reduction sequences $a \leadsto^{*} x$ and $a \leadsto^{*} y$,
+we can invert one side to get an equivalence in the reflexive symmetric
+transitive closure, and then invoke Church-Rosser to get the desired
+pair of reductions.
+
+```agda
+church-rosser→confluent : has-church-rosser R → is-confluent R
+church-rosser→confluent church-rosser a→*x a→*y =
+  church-rosser $
+    transitive
+      (symmetric (refl-trans→refl-sym-trans a→*x))
+      (refl-trans→refl-sym-trans a→*y)
+```
+
+The converse is much more tricky, and requires introducing an intermediate
+notion of **semiconfluence**, which yields solutions to diamonds of the
+following form.
+
+~~~{.quiver}
+\begin{tikzcd}
+  a && y \\
+  \\
+  x && {\exists z}
+  \arrow["{*}"', from=1-1, to=3-1]
+  \arrow["{*}"', dashed, from=3-1, to=3-3]
+  \arrow["{*}", dashed, from=1-3, to=3-3]
+  \arrow[from=1-1, to=1-3]
+\end{tikzcd}
+~~~
+
+```agda
+is-semi-confluent : (A → A → Type ℓ) → Type _
+is-semi-confluent {A = A} R =
+  ∀ {a x y} → Refl-trans R a x → R a y
+  → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z)
+```
+
+Confluence obviously implies semi-confluence.
+
+```agda
+confluent→semiconfluent : is-confluent R → is-semi-confluent R
+confluent→semiconfluent conf a→*x a→y = conf a→*x [ a→y ]
+```
+
+Furthermore, semi-confluence implies Church-Rosser. Let $\leadsto$ be a
+semi-confluent rewriting system, and let $x \leftrightarrow^{*} y$ be a
+pair of convertible elements. We proceed by inducting over the reduction
+chain $x \leftrightarrow^{*} y$. If the chain is empty, then we can
+form the trivial diamond, and we are done.
+
+If we have a reduction chain $x \to x' \leftrightarrow^{*} y$, then
+can perform induction on the $x' \leftrightarrow^{*} y$ to obtain
+a $v$ with $x' \to^{*} v$ and $y \to^{*} v$, as in the following diagram.
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {x'} && y \\
+  \\
+  && v
+  \arrow["{*}"{description}, from=1-3, to=3-3]
+  \arrow["{*}"{description}, from=1-5, to=3-3]
+  \arrow["{*}"{description}, tail reversed, from=1-3, to=1-5]
+  \arrow[from=1-1, to=1-3]
+\end{tikzcd}
+~~~
+
+Let's re-arrange the diagram a bit, adding in a trivial reduction
+of $v$ to $v$.
+
+~~~{.quiver}
+\begin{tikzcd}
+        {x'} && x && {x'} && y \\
+        \\
+        && v && v
+        \arrow["{*}"{description}, from=1-5, to=3-5]
+        \arrow["{*}"{description}, from=1-7, to=3-5]
+        \arrow["{*}"{description}, tail reversed, from=1-5, to=1-7]
+        \arrow[from=1-3, to=1-5]
+        \arrow[from=1-3, to=1-1]
+        \arrow["{*}"{description}, from=1-3, to=3-3]
+        \arrow["{*}"{description}, from=3-5, to=3-3]
+\end{tikzcd}
+~~~
+
+We can then apply semi-confluence to the pair $x \to x'$ and $x \to^{*} v$
+to get some $w$ with reductions $x' \to^{*} w$ and $v \to^{*} w$.
+
+~~~{.quiver}
+\begin{tikzcd}
+  {x'} && x && {x'} && y \\
+  \\
+  && v && v
+  \arrow["{*}"{description}, from=1-5, to=3-5]
+  \arrow["{*}"{description}, from=1-7, to=3-5]
+  \arrow["{*}"{description}, tail reversed, from=1-5, to=1-7]
+  \arrow[from=1-3, to=1-5]
+  \arrow[from=1-3, to=1-1]
+  \arrow["{*}"{description}, from=1-3, to=3-3]
+  \arrow["{*}"{description}, from=3-5, to=3-3]
+\end{tikzcd}
+~~~
+
+This yields a pair of reductions $x \to^{*} w$ and $y \to^{*} w$,
+completing this case.
+
+~~~{.quiver}
+\begin{tikzcd}
+  {x'} && x && {x'} && y \\
+  \\
+  w && v && v
+  \arrow["{*}"{description}, from=1-5, to=3-5]
+  \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=1-7, to=3-5]
+  \arrow["{*}"{description}, tail reversed, from=1-5, to=1-7]
+  \arrow[from=1-3, to=1-5]
+  \arrow[color={rgb,255:red,214;green,92;blue,92}, from=1-3, to=1-1]
+  \arrow["{*}"{description}, from=1-3, to=3-3]
+  \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=3-5, to=3-3]
+  \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=3-3, to=3-1]
+  \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=1-1, to=3-1]
+\end{tikzcd}
+~~~
+
+Finally, suppose we have a reduction chain $x' \to x \leftrightarrow^{*} y$.
+We can perform induction on the $x \leftrightarrow^{*} y$ to obtain
+a $v$ with $x \to^{*} v$ and $y \to^{*} v$, as in the following diagram.
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {x'} && y \\
+  \\
+  && v
+  \arrow["{*}"{description}, from=1-3, to=3-3]
+  \arrow["{*}"{description}, from=1-5, to=3-3]
+  \arrow["{*}"{description}, tail reversed, from=1-3, to=1-5]
+  \arrow[from=1-3, to=1-1]
+\end{tikzcd}
+~~~
+
+We can then apply semi-confluence to the reduction pair $x \to x'$ and
+$x \to^{*} v$, yielding the following diagram.
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {x'} && y \\
+  \\
+  w && v
+  \arrow["{*}"{description}, from=1-3, to=3-3]
+  \arrow["{*}"{description}, from=1-5, to=3-3]
+  \arrow["{*}"{description}, tail reversed, from=1-3, to=1-5]
+  \arrow[from=1-3, to=1-1]
+  \arrow["{*}"{description}, from=1-1, to=3-1]
+  \arrow["{*}"{description}, from=3-3, to=3-1]
+\end{tikzcd}
+~~~
+
+We can then chase some arrows to determine that we have constructed
+a pair of reductions $x \to^{*} w$ and $y \to^{*} w$, completing the proof.
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {x'} && y \\
+  \\
+  w && v
+  \arrow["{*}"{description}, from=1-3, to=3-3]
+  \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=1-5, to=3-3]
+  \arrow["{*}"{description}, tail reversed, from=1-3, to=1-5]
+  \arrow[color={rgb,255:red,214;green,92;blue,92}, from=1-3, to=1-1]
+  \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=1-1, to=3-1]
+  \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=3-3, to=3-1]
+\end{tikzcd}
+~~~
+
+```agda
+semiconfluent→church-rosser : is-semi-confluent R → has-church-rosser R
+semiconfluent→church-rosser {R = R} semiconf x↔y =
+  Refl-sym-trans-rec-chain
+    (λ x y →  ∃[ z ∈ _ ] (Refl-trans R x z × Refl-trans R y z))
+    (inc (_ , reflexive , reflexive))
+    (λ {x} {x'} {y} x→x' _ x'→*v*←y → do
+      v , x'→*v , y→*v ← x'→*v*←y
+      w , v→*w , x'→*w ← semiconf (transitive [ x→x' ] x'→*v) x→x'
+      pure (w , transitive [ x→x' ] x'→*w , transitive y→*v v→*w))
+    (λ {x} {x'} {y} x'→x _ x'→*v*←y → do
+      v , x'→*v , y→*v ← x'→*v*←y
+      w , v→*w , x→*w ← semiconf x'→*v x'→x 
+      pure (w , x→*w , transitive y→*v v→*w))
+    squash
+    x↔y
+```
+
+We can use these 3 proofs to show that confluence, Church-Rosser, and
+semi-confluence are equivalent.
+
+```agda
+semiconfluent→confluent : is-semi-confluent R → is-confluent R
+semiconfluent→confluent conf =
+  church-rosser→confluent (semiconfluent→church-rosser conf)
+
+confluent→church-rosser : is-confluent R → has-church-rosser R
+confluent→church-rosser conf =
+  semiconfluent→church-rosser (confluent→semiconfluent conf)
+
+church-rosser→semiconfluent : has-church-rosser R → is-semi-confluent R
+church-rosser→semiconfluent church-rosser =
+  confluent→semiconfluent (church-rosser→confluent church-rosser)
+```
+
+## Local Confluence and Newman's Lemma
+
+Proving confluence can be difficult, as it requires looking at
+forks of arbitrary depth. It is much easier to only consider single-step
+forks, which leads to a notion of **local confluence**.
+
+```agda
+is-locally-confluent : (A → A → Type ℓ) → Type _
+is-locally-confluent {A = A} R =
+  ∀ {a x y} → R a x → R a y
+  → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z)
+```
+
+Note that local confluence is a weaker property than confluence. As
+a concrete example, consider the following rewrite system:
+
+~~~{.quiver}
+\begin{tikzcd}
+  w & x && y & z \\
+  \\
+  \\
+  && {}
+  \arrow[curve={height=-12pt}, from=1-2, to=1-4]
+  \arrow[curve={height=-12pt}, from=1-4, to=1-2]
+  \arrow[from=1-2, to=1-1]
+  \arrow[from=1-4, to=1-5]
+\end{tikzcd}
+~~~
+
+There are two single-step forks in this system:
+$w \leftarrow x \rightarrow y$ and $x \leftarrow y \to z$. Both of
+these are locally confluent: We can reduce both to $w$ for the first fork,
+and $z$ for the second. However, it is *not* confluent: there is a fork
+$w \leftarrow^{*} x \to^{*} z$ that cannot be reconciled.
+
+However, if the rewrite system is [strongly normalising], then local
+confluence implies confluence.
+
+[strongly normalising]: Rewriting.StronglyNormalising.html
+
+Let $\to$ be a strongly normalising, locally confluent rewriting system.
+Consider some fork $x \leftarrow^{*} a \to^{*} y$. As $\to$ is strongly
+normalizing, we can perform well-founded induction, attempting to
+produce a common reduct for both sides of the fork.
+
+If either side of tthe fork is a zero-length chain, then we can use the
+trivial joins $a \to{*} x \leftarrow^{*} a$ and $a \to{*} y
+\leftarrow^{*} a$, resp.  If both chains are non-trivial, we end up with
+the following diagram:
+
+~~~{.quiver}
+\begin{tikzcd}
+  && a \\
+  & {x'} && {y'} \\
+  x &&&& y
+  \arrow[from=1-3, to=2-2]
+  \arrow[from=1-3, to=2-4]
+  \arrow["{*}"{description}, from=2-2, to=3-1]
+  \arrow["{*}"{description}, from=2-4, to=3-5]
+\end{tikzcd}
+~~~
+
+We can then apply local confluence to $a \to x'$ and $a \to y'$.
+
+~~~{.quiver}
+\begin{tikzcd}
+  && a \\
+  & {x'} && {y'} \\
+  x && u && y
+  \arrow[from=1-3, to=2-2]
+  \arrow[from=1-3, to=2-4]
+  \arrow["{*}"{description}, from=2-2, to=3-1]
+  \arrow["{*}"{description}, from=2-4, to=3-5]
+  \arrow["{*}"{description}, from=2-2, to=3-3]
+  \arrow["{*}"{description}, from=2-4, to=3-3]
+\end{tikzcd}
+~~~
+
+Next, we can recurse on $x' \to^{*} x$ and $x' \to^{*} u$.
+
+~~~{.quiver}
+\begin{tikzcd}
+  && a \\
+  & {x'} && {y'} \\
+  x && u && y \\
+  & v
+  \arrow[from=1-3, to=2-2]
+  \arrow[from=1-3, to=2-4]
+  \arrow["{*}"{description}, from=2-2, to=3-1]
+  \arrow["{*}"{description}, from=2-4, to=3-5]
+  \arrow["{*}"{description}, from=2-2, to=3-3]
+  \arrow["{*}"{description}, from=2-4, to=3-3]
+  \arrow["{*}"{description}, from=3-1, to=4-2]
+  \arrow["{*}"{description}, from=3-3, to=4-2]
+\end{tikzcd}
+~~~
+
+We can recurse yet again on $y' \to^{*} v$ and $y' \to^{*} y$.
+
+~~~{.quiver}
+\begin{tikzcd}
+  && a \\
+  & {x'} && {y'} \\
+  x && u && y \\
+  & v \\
+  && w
+  \arrow[from=1-3, to=2-2]
+  \arrow[from=1-3, to=2-4]
+  \arrow["{*}"{description}, from=2-2, to=3-1]
+  \arrow["{*}"{description}, from=2-4, to=3-5]
+  \arrow["{*}"{description}, from=2-2, to=3-3]
+  \arrow["{*}"{description}, from=2-4, to=3-3]
+  \arrow["{*}"{description}, from=3-1, to=4-2]
+  \arrow["{*}"{description}, from=3-3, to=4-2]
+  \arrow["{*}"{description}, from=3-5, to=5-3]
+  \arrow["{*}"{description}, from=4-2, to=5-3]
+\end{tikzcd}
+~~~
+
+The bottom half of the square yields the desired pair of reductions,
+finishing the proof.
+
+~~~{.quiver}
+\begin{tikzcd}
+\begin{tikzcd}
+  && a \\
+  & {x'} && {y'} \\
+  x && u && y \\
+  & v \\
+  && w
+  \arrow[from=1-3, to=2-2]
+  \arrow[from=1-3, to=2-4]
+  \arrow["{*}"{description}, from=2-2, to=3-1]
+  \arrow["{*}"{description}, from=2-4, to=3-5]
+  \arrow["{*}"{description}, from=2-2, to=3-3]
+  \arrow["{*}"{description}, from=2-4, to=3-3]
+  \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=3-1, to=4-2]
+  \arrow["{*}"{description}, from=3-3, to=4-2]
+  \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=3-5, to=5-3]
+  \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=4-2, to=5-3]
+\end{tikzcd}\end{tikzcd}
+~~~
+
+```agda
+strong-normalising+locally-confluent→confluent
+  : is-strongly-normalising R → is-locally-confluent R
+  → is-confluent R
+strong-normalising+locally-confluent→confluent
+  {R = R} sn local-conf {a} {x} {z} a→*x a→*y =
+    Wf-induction _ sn
+      (λ a →
+        ∀ {x y} → Refl-trans R a x → Refl-trans R a y
+        → ∃[ z ∈ _ ] (Refl-trans R x z × Refl-trans R y z))
+    (λ a ih {x} {y} a→*x a→*y →
+      Refl-trans-case-fork
+        (λ a x y
+          → (∀ a' → Trans R a a'
+             → ∀ {x y} → Refl-trans R a' x → Refl-trans R a' y
+             → ∃[ z ∈ _ ] (Refl-trans R x z × Refl-trans R y z))
+          → ∃[ z ∈ _ ] (Refl-trans R x z × Refl-trans R y z))
+        (λ a→*y _ → inc (_ , a→*y , reflexive))
+        (λ a→*x _ → inc (_ , reflexive , a→*x))
+        (λ a→x' x'→*x a→y' y'→*y ih → do
+          u , x'→*u , y'→*u ← local-conf a→x' a→y'
+          v , x→*v , u→*v ← ih _ [ a→x' ] x'→*x x'→*u
+          w , v→*w , y→*w ← ih _ [ a→y' ] (transitive y'→*u u→*v) y'→*y
+          pure (w , transitive x→*v v→*w , y→*w))
+        hlevel!
+        a→*x a→*y ih)
+      a a→*x a→*y
+```
diff --git a/src/Rewriting/StronglyNormalising.lagda.md b/src/Rewriting/StronglyNormalising.lagda.md
new file mode 100644
index 000000000..ef1c5e327
--- /dev/null
+++ b/src/Rewriting/StronglyNormalising.lagda.md
@@ -0,0 +1,82 @@
+<!--
+```agda
+open import 1Lab.Prelude
+open import Data.Dec
+open import Data.Rel.Closure
+open import Data.Wellfounded.Base
+```
+-->
+
+```agda
+module Rewriting.StronglyNormalising where
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  _↝_ : A → A → Type ℓ
+```
+-->
+
+# Strongly Normalising Rewrite Systems
+
+An abstract rewriting system is **strongly normalising** if its
+[transitive closure] is a [well-founded relation].
+
+[transitive closure]: Data.Rel.Closure.html#transitive-closure
+[well-founded relation]: Data.Wellfounded.Base.html
+
+```agda
+is-strongly-normalising : (A → A → Type ℓ) → Type _
+is-strongly-normalising _↝_ = Wf (λ x y → Trans _↝_ y x)
+```
+
+This definition is classically equivalent to the non-existence of infinite
+reduction sequences. However, strong normalisation is more useful
+constructively, as we can use it to perform induction. However, the
+latter notion is still useful; we call such rewrite systems **terminating**.
+
+```agda
+is-terminating : (A → A → Type ℓ) → Type _
+is-terminating {A = A} _↝_ = 
+  ¬ (∃[ aₙ ∈ (Nat → A) ] (∀ n → Trans _↝_ (aₙ n) (aₙ (suc n))))
+```
+
+If a rewrite system is strongly normalising, then it is terminating.
+Aiming for a contradiction, let us assume that we have some infinite
+chain $a_0 \leadsto a_1 \leadsto \cdots$ of reductions. We then perform
+well-founded induction where our motive states that, for all $n$, there
+is no reduction $a \leadsto^{+} a_{n+1}$. The induction step proceeds
+by recurring on $a_{n+1}$, which steps to $a_{n+2}$. This has the effect
+of following the infinite chain of reductions, leading to a divergence.
+We can extract the proof of false by applying this induction to the
+step $a_0 \leadsto a_1$ of the sequence.
+
+```agda
+strongly-normalising→terminating : is-strongly-normalising _↝_ → is-terminating _↝_
+strongly-normalising→terminating {_↝_ = _↝_} sn ∥chain∥ =
+  ∥-∥-proj $ do
+    (aₙ , step) ← ∥chain∥
+    inc $ Wf-induction _ sn
+      (λ a → ∀ n → ¬ Trans _↝_ a (aₙ (suc n)))
+      (λ a ih n aᵢ↝aₙ₊₁ → ih (aₙ (suc n)) aᵢ↝aₙ₊₁ (suc n) (step (suc n)))
+      (aₙ 0) 0 (step zero)
+```
+
+<!-- [TODO: Reed M, 02/06/2023] Prove that they are equivalent if we assume LEM. -->
+
+We can use the prior fact to show that strongly normalising rewrite
+systems contain no loops, by using the constant sequence $a \leadsto a$
+as our infinite chain.
+
+```agda
+strongly-normalising→acyclic
+  : ∀ {A : Type ℓ} {_↝_ : A → A → Type ℓ'}
+  → is-strongly-normalising _↝_
+  → ¬ (∃[ a ∈ A ] (Trans _↝_ a a))
+strongly-normalising→acyclic sn ∥loop∥ =
+  strongly-normalising→terminating sn $
+    ∥-∥-map (λ (a , a↝a) → (λ _ → a) , λ n → a↝a) ∥loop∥
+```

From 1561da2fac752a332e2a47fd263e1022de5e1dc5 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Fri, 2 Jun 2023 17:16:47 -0700
Subject: [PATCH 07/19] fix: formatting

---
 src/Rewriting/Confluent.lagda.md | 66 ++++++++++++++++----------------
 1 file changed, 34 insertions(+), 32 deletions(-)

diff --git a/src/Rewriting/Confluent.lagda.md b/src/Rewriting/Confluent.lagda.md
index 08160c1b3..8293f8bfe 100644
--- a/src/Rewriting/Confluent.lagda.md
+++ b/src/Rewriting/Confluent.lagda.md
@@ -1,3 +1,4 @@
+<!--
 ```agda
 open import Rewriting.StronglyNormalising
 
@@ -29,9 +30,9 @@ of terms in some language, along with a collection of rules that describe
 how we can simplify terms. As an example, the untyped $\lambda$-calculus
 can be naturally presented as a term rewriting system, where only
 reduction rule is $\beta$-reduction. More abstractly, a rewriting system
-on a type $A$ is simply a relation $\leadsto$ on $A$ which encodes the
+on a type $A$ is simply a relation $\to$ on $A$ which encodes the
 rewriting rules. Sequences of rewrites are then described using the
-[reflexive transitive closure] of $\leadsto$.
+[reflexive transitive closure] of $\to$.
 
 [reflexive transitive closure]: Data.Rel.Closure.html#reflexive-transitive-closure.html
 
@@ -42,20 +43,20 @@ quite problematic if we want to use the rewriting system to simplify
 expressions. It would be useful if we could prove *some* property of the
 relation that would guarantee that this situation does not occur.
 
-This leads us to the notion of **confluence**. We say a relation $\leadsto$
-is confluent if there for all pairs of reduction chains $a \leadsto^{*} x$
-and $a \leadsto^{*} y$, there exists some $z$ such that $x \leadsto^{*} z$
-and $y \leadsto^{*} z$, as in the following diagram.
+This leads us to the notion of **confluence**. We say a relation $\to$
+is confluent if for all pairs of reduction chains $a \to^{*} x$
+and $a \to^{*} y$, there exists some $z$ such that $x \to^{*} z$
+and $y \to^{*} z$, as in the following diagram.
 
 ~~~{.quiver}
 \begin{tikzcd}
   a && y \\
   \\
   x && {\exists z}
-  \arrow["{*}"', from=1-1, to=3-1]
-  \arrow["{*}"', dashed, from=3-1, to=3-3]
-  \arrow["{*}", dashed, from=1-3, to=3-3]
-  \arrow["{*}", from=1-1, to=1-3]
+  \arrow["{*}"{description}, from=1-1, to=3-1]
+  \arrow["{*}"{description}, dashed, from=3-1, to=3-3]
+  \arrow["{*}"{description}, dashed, from=1-3, to=3-3]
+  \arrow["{*}"{description}, from=1-1, to=1-3]
 \end{tikzcd}
 ~~~
 
@@ -93,11 +94,11 @@ diverging paths by rewriting to the term at the bottom of the diagram.
 
 ## The Church-Rosser Property
 
-A rewriting system $\leadsto$ yields an equivalence relation on terms via
-the [reflexive symmetric transitive closure] of $\leadsto$. This leads to
+A rewriting system $\to$ yields an equivalence relation on terms via
+the [reflexive symmetric transitive closure] of $\to$. This leads to
 a variant of confluence known as the **Church-Rosser Property**, which
 requires a $z$ for every pair of equivalent terms $x$ and $y$ such that
-$x \leadsto^{z}$ and $y \leadsto^{z}$.
+$x \to^{*} z$ and $y \to^{*} z$.
 
 [reflexive symmetric transitive closure]: Data.Rel.Closure.html#reflexive-symmetric-transitive-closure.html
 
@@ -105,9 +106,9 @@ $x \leadsto^{z}$ and $y \leadsto^{z}$.
 \begin{tikzcd}
   x && y \\
   & z
-  \arrow["{*}"', dashed, from=1-1, to=2-2]
-  \arrow["{*}", dashed, from=1-3, to=2-2]
-  \arrow["{*}", tail reversed, from=1-1, to=1-3]
+  \arrow["{*}"{description}, dashed, from=1-1, to=2-2]
+  \arrow["{*}"{description}, dashed, from=1-3, to=2-2]
+  \arrow["{*}"{description}, tail reversed, from=1-1, to=1-3]
 \end{tikzcd}
 ~~~
 
@@ -126,16 +127,16 @@ as Church-Rosser also gives us diamonds of the following shape:
   a && y \\
   \\
   x && {\exists z}
-  \arrow["{*}", from=3-1, to=1-1]
-  \arrow["{*}"', dashed, from=3-1, to=3-3]
-  \arrow["{*}", dashed, from=1-3, to=3-3]
-  \arrow["{*}"', from=1-3, to=1-1]
+  \arrow["{*}"{description}, from=3-1, to=1-1]
+  \arrow["{*}"{description}', dashed, from=3-1, to=3-3]
+  \arrow["{*}"{description}, dashed, from=1-3, to=3-3]
+  \arrow["{*}"{description}, from=1-3, to=1-1]
 \end{tikzcd}
 ~~~
 
 Somewhat surprisingly, it turns out that the two conditions are equivalent!
 Showing that Church-Rosser implies confluence is rather easy: if we
-have two reduction sequences $a \leadsto^{*} x$ and $a \leadsto^{*} y$,
+have two reduction sequences $a \to^{*} x$ and $a \to^{*} y$,
 we can invert one side to get an equivalence in the reflexive symmetric
 transitive closure, and then invoke Church-Rosser to get the desired
 pair of reductions.
@@ -150,7 +151,7 @@ church-rosser→confluent church-rosser a→*x a→*y =
 ```
 
 The converse is much more tricky, and requires introducing an intermediate
-notion of **semiconfluence**, which yields solutions to diamonds of the
+notion of **semi-confluence**, which yields solutions to diamonds of the
 following form.
 
 ~~~{.quiver}
@@ -158,9 +159,9 @@ following form.
   a && y \\
   \\
   x && {\exists z}
-  \arrow["{*}"', from=1-1, to=3-1]
-  \arrow["{*}"', dashed, from=3-1, to=3-3]
-  \arrow["{*}", dashed, from=1-3, to=3-3]
+  \arrow["{*}"{description}, from=1-1, to=3-1]
+  \arrow["{*}"{description}', dashed, from=3-1, to=3-3]
+  \arrow["{*}"{description}, dashed, from=1-3, to=3-3]
   \arrow[from=1-1, to=1-3]
 \end{tikzcd}
 ~~~
@@ -179,7 +180,7 @@ confluent→semiconfluent : is-confluent R → is-semi-confluent R
 confluent→semiconfluent conf a→*x a→y = conf a→*x [ a→y ]
 ```
 
-Furthermore, semi-confluence implies Church-Rosser. Let $\leadsto$ be a
+Furthermore, semi-confluence implies Church-Rosser. Let $\to$ be a
 semi-confluent rewriting system, and let $x \leftrightarrow^{*} y$ be a
 pair of convertible elements. We proceed by inducting over the reduction
 chain $x \leftrightarrow^{*} y$. If the chain is empty, then we can
@@ -226,7 +227,7 @@ to get some $w$ with reductions $x' \to^{*} w$ and $v \to^{*} w$.
 \begin{tikzcd}
   {x'} && x && {x'} && y \\
   \\
-  && v && v
+  w && v && v
   \arrow["{*}"{description}, from=1-5, to=3-5]
   \arrow["{*}"{description}, from=1-7, to=3-5]
   \arrow["{*}"{description}, tail reversed, from=1-5, to=1-7]
@@ -234,6 +235,8 @@ to get some $w$ with reductions $x' \to^{*} w$ and $v \to^{*} w$.
   \arrow[from=1-3, to=1-1]
   \arrow["{*}"{description}, from=1-3, to=3-3]
   \arrow["{*}"{description}, from=3-5, to=3-3]
+  \arrow["{*}"{description}, from=3-3, to=3-1]
+  \arrow["{*}"{description}, from=1-1, to=3-1]
 \end{tikzcd}
 ~~~
 
@@ -422,7 +425,7 @@ We can then apply local confluence to $a \to x'$ and $a \to y'$.
 
 Next, we can recurse on $x' \to^{*} x$ and $x' \to^{*} u$.
 
-~~~{.quiver}
+~~~{.quiver .tall-2}
 \begin{tikzcd}
   && a \\
   & {x'} && {y'} \\
@@ -441,7 +444,7 @@ Next, we can recurse on $x' \to^{*} x$ and $x' \to^{*} u$.
 
 We can recurse yet again on $y' \to^{*} v$ and $y' \to^{*} y$.
 
-~~~{.quiver}
+~~~{.quiver .tall-2}
 \begin{tikzcd}
   && a \\
   & {x'} && {y'} \\
@@ -464,8 +467,7 @@ We can recurse yet again on $y' \to^{*} v$ and $y' \to^{*} y$.
 The bottom half of the square yields the desired pair of reductions,
 finishing the proof.
 
-~~~{.quiver}
-\begin{tikzcd}
+~~~{.quiver .tall-2}
 \begin{tikzcd}
   && a \\
   & {x'} && {y'} \\
@@ -482,7 +484,7 @@ finishing the proof.
   \arrow["{*}"{description}, from=3-3, to=4-2]
   \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=3-5, to=5-3]
   \arrow["{*}"{description}, color={rgb,255:red,214;green,92;blue,92}, from=4-2, to=5-3]
-\end{tikzcd}\end{tikzcd}
+\end{tikzcd}
 ~~~
 
 ```agda

From ad7cf0666007ce7c378b51123b57f6f4623cb7bb Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Mon, 26 Jun 2023 11:48:33 -0700
Subject: [PATCH 08/19] def: relations

---
 src/Data/Rel/Base.lagda.md | 73 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 73 insertions(+)
 create mode 100644 src/Data/Rel/Base.lagda.md

diff --git a/src/Data/Rel/Base.lagda.md b/src/Data/Rel/Base.lagda.md
new file mode 100644
index 000000000..7a567a453
--- /dev/null
+++ b/src/Data/Rel/Base.lagda.md
@@ -0,0 +1,73 @@
+<!--
+```agda
+open import 1Lab.Prelude
+open import Data.Sum
+```
+-->
+
+```agda
+module Data.Rel.Base where
+```
+
+# Relations
+
+A **relation** between types $A$ and $B$ consists of a family of types
+indexed by $A$ and $B$.
+
+```agda
+Rel : ∀ {a b} → Type a → Type b → (ℓ : Level) → Type _
+Rel A B ℓ = A → B → Type ℓ
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' : Level
+  A B C : Type ℓ
+  R S : Rel A B ℓ
+```
+-->
+
+## Operations on Relations
+
+We can take the union of two relations by taking the pointwise truncated
+coproduct.
+
+```agda
+_∪r_ : Rel A B ℓ → Rel A B ℓ' → Rel A B _
+R ∪r S = λ x y → ∥ R x y ⊎ S x y ∥
+```
+
+Likewise, intersection can be defined by taking the pointwise product
+of the two relations.
+
+```agda
+_∩r_ : Rel A B ℓ → Rel A B ℓ' → Rel A B _
+R ∩r S = λ x y → R x y × S x y
+```
+
+We can compose two relations by requiring the (mere) existence of a
+common endpoint.
+
+```agda
+_∘r_ : Rel B C ℓ → Rel A B ℓ' → Rel A C _
+R ∘r S = λ x y → ∃[ z ∈ _ ] (S x z × R z y)
+```
+
+Every relation between $A$ and $B$ can be flipped to get a relation
+between $B$ and $A$.
+
+```agda
+flipr : Rel A B ℓ → Rel B A ℓ
+flipr R = λ x y → R y x
+```
+
+## Relationships between Relations
+
+We say that a relation $R$ is contained in another relation $S$
+if $R(x,y)$ implies $S(x,y)$ for every $x$ and $y$.
+
+```agda
+_⊆r_ : Rel A B ℓ → Rel A B ℓ' → Type _
+R ⊆r S = ∀ {x y} → R x y → S x y
+```

From 320d84929fd27c785f091fdb16bcfb94d3decb6f Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Mon, 26 Jun 2023 13:01:40 -0700
Subject: [PATCH 09/19] def: a bunch of random properties of closure

---
 src/Data/Rel/Base.lagda.md    |  52 ++++++++-
 src/Data/Rel/Closure.lagda.md | 200 ++++++++++++++++++++++++++--------
 2 files changed, 205 insertions(+), 47 deletions(-)

diff --git a/src/Data/Rel/Base.lagda.md b/src/Data/Rel/Base.lagda.md
index 7a567a453..ce8adce5c 100644
--- a/src/Data/Rel/Base.lagda.md
+++ b/src/Data/Rel/Base.lagda.md
@@ -28,9 +28,18 @@ private variable
 ```
 -->
 
-## Operations on Relations
+We say that a relation is **propositional** if $R(x,y)$ is a proposition
+for every $x$ and $y$.
 
-We can take the union of two relations by taking the pointwise truncated
+```agda
+is-prop-rel : Rel A B ℓ → Type _
+is-prop-rel R = ∀ {x y} → is-prop (R x y)
+```
+
+## Operations on Propositional Relations
+
+We can take the union of two propositional relations by taking the
+pointwise truncated
 coproduct.
 
 ```agda
@@ -46,8 +55,8 @@ _∩r_ : Rel A B ℓ → Rel A B ℓ' → Rel A B _
 R ∩r S = λ x y → R x y × S x y
 ```
 
-We can compose two relations by requiring the (mere) existence of a
-common endpoint.
+We can compose two propositional relations by requiring the (mere)
+existence of a common endpoint.
 
 ```agda
 _∘r_ : Rel B C ℓ → Rel A B ℓ' → Rel A C _
@@ -71,3 +80,38 @@ if $R(x,y)$ implies $S(x,y)$ for every $x$ and $y$.
 _⊆r_ : Rel A B ℓ → Rel A B ℓ' → Type _
 R ⊆r S = ∀ {x y} → R x y → S x y
 ```
+
+Equality of propositional relations can be characterised in terms
+of containment.
+
+```agda
+prop-rel-ext
+  : is-prop-rel R → is-prop-rel S
+  → R ⊆r S → S ⊆r R → R ≡ S
+prop-rel-ext R-prop S-prop R⊆S S⊆R =
+  funext λ x → funext λ y → ua (prop-ext R-prop S-prop R⊆S S⊆R)
+```
+
+## Properties of Relations
+
+A relation is **reflexive** if every element is related to itself.
+
+```agda
+is-reflexive : Rel A A ℓ → Type _
+is-reflexive R = ∀ x → R x x
+```
+
+A relation is **symmetric** if every $R(x,y)$ implies that $R(y,x)$.
+
+```agda
+is-symmetric : Rel A A ℓ → Type _
+is-symmetric R = ∀ {x y} → R x y → R y x
+```
+
+A relation is **transitive** if $R(x,y)$ and $R(y,z)$ implies that
+$R(x,z)$.
+
+```agda
+is-transitive : Rel A A ℓ → Type _
+is-transitive R = ∀ {x y z} → R x y → R y z → R x z
+```
diff --git a/src/Data/Rel/Closure.lagda.md b/src/Data/Rel/Closure.lagda.md
index 4ab7a7a08..950fb599b 100644
--- a/src/Data/Rel/Closure.lagda.md
+++ b/src/Data/Rel/Closure.lagda.md
@@ -3,6 +3,8 @@
 open import 1Lab.Prelude
 open import Data.Sum
 
+open import Data.Rel.Base
+
 import Data.Nat as Nat
 import Data.Nat.Order as Nat
 ```
@@ -17,7 +19,7 @@ module Data.Rel.Closure where
 private variable
   ℓ ℓ' ℓ'' : Level
   A B X : Type ℓ
-  R S : A → A → Type ℓ
+  R R' S : A → A → Type ℓ
 ```
 -->
 
@@ -35,7 +37,7 @@ The reflexive closure of a relation $R$ is the smallest reflexive
 relation $R^{=}$ that contains $R$.
 
 ```agda
-data Refl {A : Type ℓ} (R : A → A → Type ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where
+data Refl {A : Type ℓ} (R : Rel A A ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where
   reflexive : Refl R x x
   [_] : ∀ {y} → R x y → Refl R x y
   trunc : ∀ {y} → is-prop (Refl R x y)
@@ -80,33 +82,52 @@ Refl-rec {R = R} S prel prefl pprop r+ = go r+ where
   go (trunc r+ r+' i) = pprop (go r+) (go r+') i
 ```
 
+<!--
+```agda
+Refl-rec₂
+  : (S : A → A → A → Type ℓ)
+  → (∀ {x y z} → R x y → R' y z → S x y z)
+  → (∀ {x z} → R' x z → S x x z)
+  → (∀ {x y} → R x y → S x y y)
+  → (∀ x → S x x x)
+  → (∀ {x y z} → is-prop (S x y z))
+  → ∀ {x y z} → Refl R x y → Refl R' y z → S x y z
+Refl-rec₂ {R = R} {R' = R'} S prel prefll preflr prefl2 pprop r+ r+' = go r+ r+' where
+  go : ∀ {x y z} → Refl R x y → Refl R' y z → S x y z
+  go reflexive reflexive = prefl2 _
+  go reflexive [ r' ] = prefll r'
+  go reflexive (trunc r+ r+' i) =
+    pprop (go reflexive r+) (go reflexive r+') i
+  go [ r ] reflexive = preflr r
+  go [ r ] [ r' ] = prel r r'
+  go [ r ] (trunc r+ r+' i) =
+    pprop (go [ r ] r+) (go [ r ] r+') i
+  go (trunc r+ r+' i) r+'' =
+    pprop (go r+ r+'') (go r+' r+'') i
+```
+-->
+
 If the original relation is symmetric or transitive, then so is the
 reflexive closure.
 
 ```agda
 refl-clo-symmetric
-  : (∀ {x y} → R x y → R y x)
-  → ∀ {x y} → Refl R x y → Refl R y x
+  : is-symmetric R
+  → is-symmetric (Refl R)
 refl-clo-symmetric {R = R} is-sym =
   Refl-rec (λ x y → Refl R y x)
     (λ r → [ is-sym r ])
     (λ _ → reflexive)
     trunc
 
-refl-clo-transitive
-  : (∀ {x y z} → R x y → R y z → R x z)
-  → ∀ {x y z} → Refl R x y → Refl R y z → Refl R x z
-refl-clo-transitive is-trans reflexive s+ = s+
-refl-clo-transitive is-trans [ r ] reflexive = [ r ]
-refl-clo-transitive is-trans [ r ] [ s ] = [ is-trans r s ]
-refl-clo-transitive is-trans [ r ] (trunc s+ s+' i) =
-  trunc
-    (refl-clo-transitive is-trans [ r ] s+)
-    (refl-clo-transitive is-trans [ r ] s+') i
-refl-clo-transitive is-trans (trunc r+ r+' i) s+ =
-  trunc
-    (refl-clo-transitive is-trans r+ s+)
-    (refl-clo-transitive is-trans r+' s+) i
+refl-clo-transitive : is-transitive R → is-transitive (Refl R)
+refl-clo-transitive {R = R} is-trans =
+    Refl-rec₂ (λ x _ z → Refl R x z)
+      (λ x~*y y~*z → [ is-trans x~*y y~*z ])
+      [_]
+      [_]
+      (λ _ → reflexive)
+      hlevel!
 ```
 
 
@@ -125,7 +146,7 @@ data Sym {A : Type ℓ} (R : A → A → Type ℓ') (x y : A) : Type (ℓ ⊔ 
 <!--
 ```agda
 instance
-  Sym-H-Level : ∀ {x y} {n} → H-Level (Refl R x y) (suc n)
+  Sym-H-Level : ∀ {x y} {n} → H-Level (Sym R x y) (suc n)
   Sym-H-Level = prop-instance trunc
 
 Sym-elim
@@ -174,14 +195,10 @@ sym-clo-rel {R = R} =
     squash
 ```
 
-
-
 If the original relation is reflexive, then so is the symmetric closure.
 
 ```agda
-sym-clo-reflexive
-  : (∀ x → R x x)
-  → ∀ x → Sym R x x
+sym-clo-reflexive : is-reflexive R → is-reflexive (Sym R)
 sym-clo-reflexive is-refl x = [ is-refl x ]
 ```
 
@@ -201,7 +218,7 @@ numbers.
 ```agda
 private
   ¬sym-clo-transitive
-    : ¬ (∀ {x y z} → Sym Nat._<_ x y → Sym Nat._<_ y z → Sym Nat._<_ x z)
+    : ¬ (is-transitive (Sym Nat._<_))
   ¬sym-clo-transitive sym-clo-trans =
     ∥-∥-rec! (⊎-rec (Nat.<-irrefl refl) (Nat.<-irrefl refl))
       (sym-clo-rel (sym-clo-trans [ 0<1 ] (symmetric 0<1)))
@@ -210,6 +227,43 @@ private
       0<1 = Nat.s≤s Nat.0≤x
 ```
 
+As a corollary, we can see that the transitive closure of the symmetric closure
+is not the same as the symmetric closure of the transitive closure.
+
+However, the reflexive closure of the symmetric closure is equal to the
+symmetric closure of the reflexive closure.
+
+```agda
+sym-clo-refl-clo⊆refl-clo-sym-clo : Sym (Refl R) ⊆r Refl (Sym R)
+sym-clo-refl-clo⊆refl-clo-sym-clo {R = R} =
+  Sym-rec (Refl (Sym R))
+    (Refl-rec (Refl (Sym R))
+      (λ x~y → [ [ x~y ] ])
+      (λ _ → reflexive)
+      hlevel!)
+    (Refl-rec (flipr (Refl (Sym R)))
+      (λ y~x →  [ symmetric y~x ] )
+      (λ _ → reflexive)
+      hlevel!)
+    hlevel!
+
+refl-clo-sym-clo⊆sym-clo-refl-clo : Refl (Sym R) ⊆r Sym (Refl R)
+refl-clo-sym-clo⊆sym-clo-refl-clo {R = R} =
+  Refl-rec (Sym (Refl R))
+    (Sym-rec (Sym (Refl R))
+      (λ x~y → [ [ x~y ] ])
+      (λ x~y → symmetric [ x~y ])
+      hlevel!)
+    (λ _ → [ reflexive ])
+    hlevel!
+
+refl-clo-sym-clo≡sym-clo-refl-clo : Refl (Sym R) ≡ Sym (Refl R)
+refl-clo-sym-clo≡sym-clo-refl-clo =
+  prop-rel-ext trunc trunc
+    refl-clo-sym-clo⊆sym-clo-refl-clo
+    sym-clo-refl-clo⊆refl-clo-sym-clo
+```
+
 
 ## Transitive Closure
 
@@ -217,7 +271,7 @@ The transitive closure of a relation $R$ is the smallest transitive
 relation $R^{+}$ that contains $R$.
 
 ```agda
-data Trans {A : Type ℓ} (_~_ : A → A → Type ℓ') (x z : A) : Type (ℓ ⊔ ℓ') where
+data Trans {A : Type ℓ} (_~_ : Rel A A ℓ') (x z : A) : Type (ℓ ⊔ ℓ') where
   [_] : x ~ z → Trans _~_ x z
   transitive : ∀ {y} → Trans _~_ x y → Trans _~_ y z → Trans _~_ x z
   trunc : is-prop (Trans _~_ x z)
@@ -267,14 +321,10 @@ If the original relation is reflexive or symmetric, then so is the
 transitive closure.
 
 ```agda
-trans-clo-reflexive
-  : (∀ x → R x x)
-  → ∀ x → Trans R x x
+trans-clo-reflexive : is-reflexive R → is-reflexive (Trans R)
 trans-clo-reflexive is-refl x = [ is-refl x ]
 
-trans-clo-symmetric
-  : (∀ {x y} → R x y → R y x)
-  → ∀ {x y} → Trans R x y → Trans R y x
+trans-clo-symmetric : is-symmetric R → is-symmetric (Trans R)
 trans-clo-symmetric {R = R} is-sym r+ =
   Trans-rec (λ x y → Trans R y x)
     (λ r → [ is-sym r ])
@@ -366,16 +416,16 @@ We also provide an eliminator for inspecting forks.
 ```agda
 Refl-trans-case-fork
   : (S : A → A → A → Type ℓ)
-  → (∀ {a y} → Refl-trans R a y → S a a y)
+  → (∀ {a y} → Refl-trans R' a y → S a a y)
   → (∀ {a x} → Refl-trans R a x → S a x a)
   → (∀ {a x y x' y'}
      → R a x' → Refl-trans R x' x
-     → R a y' → Refl-trans R y' y
+     → R' a y' → Refl-trans R' y' y
      → S a x y)
   → (∀ {a x y} → is-prop (S a x y))
-  → ∀ {a x y} → Refl-trans R a x → Refl-trans R a y → S a x y
-Refl-trans-case-fork {R = R} S refll reflr fork prop {a} {x} {y} a→*x a→*y =
-  Refl-trans-rec-chain (λ a x → Refl-trans R a y → S a x y)
+  → ∀ {a x y} → Refl-trans R a x → Refl-trans R' a y → S a x y
+Refl-trans-case-fork {R' = R'} {R = R} S refll reflr fork prop {a} {x} {y} a→*x a→*y =
+  Refl-trans-rec-chain (λ a x → Refl-trans R' a y → S a x y)
     refll
     (λ {a} {a'} {x} a→a' a'→*x _ a→*y →
       Refl-trans-rec-chain
@@ -392,9 +442,7 @@ If the underlying relation is symmetric, then so is the
 reflexive-transitive closure.
 
 ```agda
-refl-trans-clo-symmetric
-  : (∀ {x y} → R x y → R y x)
-  → ∀ {x y} → Refl-trans R x y → Refl-trans R y x
+refl-trans-clo-symmetric : is-symmetric R → is-symmetric (Refl-trans R)
 refl-trans-clo-symmetric {R = R} is-sym r+ =
   Refl-trans-rec (λ x y → Refl-trans R y x)
     (λ r → [ is-sym r ])
@@ -404,6 +452,72 @@ refl-trans-clo-symmetric {R = R} is-sym r+ =
     r+
 ```
 
+The reflexive closure and the transitive closure are contained in
+the reflexive transitive closure.
+
+```agda
+refl-clo⊆refl-trans-clo : Refl R ⊆r Refl-trans R
+refl-clo⊆refl-trans-clo {R = R} =
+  Refl-rec (Refl-trans R) [_] (λ _ → reflexive) hlevel!
+
+trans-clo⊆refl-trans-clo : Trans R ⊆r Refl-trans R
+trans-clo⊆refl-trans-clo {R = R} =
+  Trans-rec (Refl-trans R) [_] transitive hlevel!
+```
+
+
+Note that the reflexive-transitive closure is equivalent to taking
+the reflexive closure of the transitive closure.
+
+```agda
+refl-clo-trans-clo⊆refl-trans-clo : Refl (Trans R) ⊆r Refl-trans R
+refl-clo-trans-clo⊆refl-trans-clo {R = R} =
+  Refl-rec (Refl-trans R)
+    trans-clo⊆refl-trans-clo
+    (λ _ → reflexive)
+    hlevel!
+
+refl-trans-clo⊆refl-clo-trans-clo : Refl-trans R ⊆r Refl (Trans R)
+refl-trans-clo⊆refl-clo-trans-clo {R = R} =
+  Refl-trans-rec (Refl (Trans R))
+    (λ x~y → [ [ x~y ] ])
+    reflexive
+    (refl-clo-transitive transitive)
+    hlevel!
+
+refl-clo-trans-clo≡refl-trans-clo : Refl (Trans R) ≡ Refl-trans R
+refl-clo-trans-clo≡refl-trans-clo {R = R} =
+  prop-rel-ext trunc trunc
+    refl-clo-trans-clo⊆refl-trans-clo
+    refl-trans-clo⊆refl-clo-trans-clo
+```
+
+The same can be said for the transitive closure of the reflexive closure.
+
+```agda
+trans-clo-refl-clo⊆refl-trans-clo : Trans (Refl R) ⊆r Refl-trans R
+trans-clo-refl-clo⊆refl-trans-clo {R = R} =
+  Trans-rec (Refl-trans R)
+    refl-clo⊆refl-trans-clo
+    transitive
+    hlevel!
+
+refl-trans-clo⊆trans-clo-refl-clo : Refl-trans R ⊆r Trans (Refl R)
+refl-trans-clo⊆trans-clo-refl-clo {R = R} =
+  Refl-trans-rec (Trans (Refl R))
+    (λ x~y → [ [ x~y ] ])
+    [ reflexive ]
+    transitive
+    hlevel!
+
+trans-clo-refl-clo≡refl-trans-clo : Trans (Refl R) ≡ Refl-trans R
+trans-clo-refl-clo≡refl-trans-clo {R = R} =
+  prop-rel-ext trunc trunc
+    trans-clo-refl-clo⊆refl-trans-clo
+    refl-trans-clo⊆trans-clo-refl-clo
+```
+
+
 ## Reflexive-Symmetric-Transitive Closure
 
 Finally, the reflexive-symmetric-transitive closure of a relation $R$ is
@@ -505,8 +619,8 @@ The reflexive-transitive closure embeds into the reflexive symmetric
 transitive closure.
 
 ```agda
-refl-trans→refl-sym-trans
-  : ∀ {x y} → Refl-trans R x y → Refl-sym-trans R x y
-refl-trans→refl-sym-trans =
+refl-trans⊆refl-sym-trans
+  : Refl-trans R ⊆r Refl-sym-trans R
+refl-trans⊆refl-sym-trans =
   Refl-trans-rec (Refl-sym-trans _) [_] reflexive transitive trunc
 ```

From db049f0c68e4dc1c73520c10ba62f3cf472d2019 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Mon, 26 Jun 2023 15:17:30 -0700
Subject: [PATCH 10/19] def: reorganize closures of relations

---
 src/Data/Rel/Base.lagda.md                    |   8 +-
 src/Data/Rel/Closure.agda                     |  12 +
 src/Data/Rel/Closure.lagda.md                 | 626 ------------------
 src/Data/Rel/Closure/Base.lagda.md            |  80 +++
 src/Data/Rel/Closure/Reflexive.lagda.md       | 146 ++++
 .../ReflexiveSymmetricTransitive.lagda.md     | 164 +++++
 .../Rel/Closure/ReflexiveTransitive.lagda.md  | 212 ++++++
 src/Data/Rel/Closure/Symmetric.lagda.md       | 189 ++++++
 src/Data/Rel/Closure/Transitive.lagda.md      | 113 ++++
 9 files changed, 923 insertions(+), 627 deletions(-)
 create mode 100644 src/Data/Rel/Closure.agda
 delete mode 100644 src/Data/Rel/Closure.lagda.md
 create mode 100644 src/Data/Rel/Closure/Base.lagda.md
 create mode 100644 src/Data/Rel/Closure/Reflexive.lagda.md
 create mode 100644 src/Data/Rel/Closure/ReflexiveSymmetricTransitive.lagda.md
 create mode 100644 src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
 create mode 100644 src/Data/Rel/Closure/Symmetric.lagda.md
 create mode 100644 src/Data/Rel/Closure/Transitive.lagda.md

diff --git a/src/Data/Rel/Base.lagda.md b/src/Data/Rel/Base.lagda.md
index ce8adce5c..5c0ddeeb8 100644
--- a/src/Data/Rel/Base.lagda.md
+++ b/src/Data/Rel/Base.lagda.md
@@ -24,7 +24,7 @@ Rel A B ℓ = A → B → Type ℓ
 private variable
   ℓ ℓ' : Level
   A B C : Type ℓ
-  R S : Rel A B ℓ
+  R S T : Rel A B ℓ
 ```
 -->
 
@@ -81,6 +81,12 @@ _⊆r_ : Rel A B ℓ → Rel A B ℓ' → Type _
 R ⊆r S = ∀ {x y} → R x y → S x y
 ```
 
+```agda
+⊆r-trans : R ⊆r S → S ⊆r T → R ⊆r T 
+⊆r-trans p q Rxy = q (p Rxy)
+```
+
+
 Equality of propositional relations can be characterised in terms
 of containment.
 
diff --git a/src/Data/Rel/Closure.agda b/src/Data/Rel/Closure.agda
new file mode 100644
index 000000000..5a88290de
--- /dev/null
+++ b/src/Data/Rel/Closure.agda
@@ -0,0 +1,12 @@
+-- This module doesn't have any text! That's because it's simply a bunch
+-- of convenient re-exports for working with closures of relations
+
+module Data.Rel.Closure where
+
+open import Data.Rel.Base public
+open import Data.Rel.Closure.Base public
+open import Data.Rel.Closure.Reflexive public
+open import Data.Rel.Closure.Symmetric public
+open import Data.Rel.Closure.Transitive public
+open import Data.Rel.Closure.ReflexiveTransitive public
+open import Data.Rel.Closure.ReflexiveSymmetricTransitive public
diff --git a/src/Data/Rel/Closure.lagda.md b/src/Data/Rel/Closure.lagda.md
deleted file mode 100644
index 950fb599b..000000000
--- a/src/Data/Rel/Closure.lagda.md
+++ /dev/null
@@ -1,626 +0,0 @@
-<!--
-```agda
-open import 1Lab.Prelude
-open import Data.Sum
-
-open import Data.Rel.Base
-
-import Data.Nat as Nat
-import Data.Nat.Order as Nat
-```
--->
-
-```agda
-module Data.Rel.Closure where
-```
-
-<!--
-```agda
-private variable
-  ℓ ℓ' ℓ'' : Level
-  A B X : Type ℓ
-  R R' S : A → A → Type ℓ
-```
--->
-
-# Closures of relations
-
-A **closure operator** $-^{+}$ on relations takes a relation $R$ on a type
-$A$ to a new relation $R^{+}$ on $A$, where $R^{+}$ is the smallest
-relation containing $R$ that satisfies some property.
-
-<!-- [TODO: Reed M, 01/06/2023] Talk about monads here. -->
-
-## Reflexive Closure
-
-The reflexive closure of a relation $R$ is the smallest reflexive
-relation $R^{=}$ that contains $R$.
-
-```agda
-data Refl {A : Type ℓ} (R : Rel A A ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where
-  reflexive : Refl R x x
-  [_] : ∀ {y} → R x y → Refl R x y
-  trunc : ∀ {y} → is-prop (Refl R x y)
-```
-
-<!--
-```agda
-instance
-  Refl-H-Level : ∀ {x y} {n} → H-Level (Refl R x y) (suc n)
-  Refl-H-Level = prop-instance trunc
-
-Refl-elim
-  : (P : ∀ (x y : A) → Refl R x y → Type ℓ'')
-  → (∀ {x y} → (r : R x y) → P x y [ r ])
-  → (∀ x → P x x reflexive)
-  → (∀ {x y} → (r+ : Refl R x y) → is-prop (P x y r+))
-  → ∀ {x y} → (r+ : Refl R x y) → P x y r+
-Refl-elim {R = R} P prel prefl pprop r+ = go r+ where
-  go : ∀ {x y} → (r+ : Refl R x y) → P x y r+
-  go reflexive = prefl _
-  go [ x ] = prel x
-  go (trunc r+ r+' i) =
-    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
-```
--->
-
-The recursion principle for the reflexive closure of a relation witnesses
-the aforementioned universal property: it is the smallest reflexive
-relation containing $R$.
-
-```agda
-Refl-rec
-  : (S : A → A → Type ℓ)
-  → (∀ {x y} → R x y → S x y)
-  → (∀ x → S x x)
-  → (∀ {x y} → is-prop (S x y))
-  → ∀ {x y} → Refl R x y → S x y
-Refl-rec {R = R} S prel prefl pprop r+ = go r+ where
-  go : ∀ {x y} → Refl R x y → S x y
-  go reflexive = prefl _
-  go [ r ] = prel r
-  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
-```
-
-<!--
-```agda
-Refl-rec₂
-  : (S : A → A → A → Type ℓ)
-  → (∀ {x y z} → R x y → R' y z → S x y z)
-  → (∀ {x z} → R' x z → S x x z)
-  → (∀ {x y} → R x y → S x y y)
-  → (∀ x → S x x x)
-  → (∀ {x y z} → is-prop (S x y z))
-  → ∀ {x y z} → Refl R x y → Refl R' y z → S x y z
-Refl-rec₂ {R = R} {R' = R'} S prel prefll preflr prefl2 pprop r+ r+' = go r+ r+' where
-  go : ∀ {x y z} → Refl R x y → Refl R' y z → S x y z
-  go reflexive reflexive = prefl2 _
-  go reflexive [ r' ] = prefll r'
-  go reflexive (trunc r+ r+' i) =
-    pprop (go reflexive r+) (go reflexive r+') i
-  go [ r ] reflexive = preflr r
-  go [ r ] [ r' ] = prel r r'
-  go [ r ] (trunc r+ r+' i) =
-    pprop (go [ r ] r+) (go [ r ] r+') i
-  go (trunc r+ r+' i) r+'' =
-    pprop (go r+ r+'') (go r+' r+'') i
-```
--->
-
-If the original relation is symmetric or transitive, then so is the
-reflexive closure.
-
-```agda
-refl-clo-symmetric
-  : is-symmetric R
-  → is-symmetric (Refl R)
-refl-clo-symmetric {R = R} is-sym =
-  Refl-rec (λ x y → Refl R y x)
-    (λ r → [ is-sym r ])
-    (λ _ → reflexive)
-    trunc
-
-refl-clo-transitive : is-transitive R → is-transitive (Refl R)
-refl-clo-transitive {R = R} is-trans =
-    Refl-rec₂ (λ x _ z → Refl R x z)
-      (λ x~*y y~*z → [ is-trans x~*y y~*z ])
-      [_]
-      [_]
-      (λ _ → reflexive)
-      hlevel!
-```
-
-
-## Symmetric Closure
-
-The symmetric closure of a relation $R$ is the smallest symmetric
-relation $R^{\leftrightarrow}$ that contains $R$.
-
-```agda
-data Sym {A : Type ℓ} (R : A → A → Type ℓ') (x y : A) : Type (ℓ ⊔ ℓ') where
-  symmetric : R y x → Sym R x y
-  [_] : R x y → Sym R x y
-  trunc : is-prop (Sym R x y)
-```
-
-<!--
-```agda
-instance
-  Sym-H-Level : ∀ {x y} {n} → H-Level (Sym R x y) (suc n)
-  Sym-H-Level = prop-instance trunc
-
-Sym-elim
-  : (P : ∀ (x y : A) → Sym R x y → Type ℓ'')
-  → (∀ {x y} → (r : R x y) → P x y [ r ])
-  → (∀ {x y} → (r : R y x) → P x y (symmetric r))
-  → (∀ {x y} → (r+ : Sym R x y) → is-prop (P x y r+))
-  → ∀ {x y} → (r+ : Sym R x y) → P x y r+
-Sym-elim {R = R} P prel psym pprop r+ = go r+ where
-  go : ∀ {x y} → (r+ : Sym R x y) → P x y r+
-  go (symmetric x) = psym x
-  go [ x ] = prel x
-  go (trunc r+ r+' i) =
-    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
-```
--->
-
-Like the reflexive closure, the recursion principle for the symmetric
-closure witnesses it's universal property; it is the smallest symmetric
-relation containing $R$.
-
-```agda
-Sym-rec
-  : (S : A → A → Type ℓ)
-  → (∀ {x y} → R x y → S x y)
-  → (∀ {x y} → R x y → S y x)
-  → (∀ {x y} → is-prop (S x y))
-  → ∀ {x y} → Sym R x y → S x y
-Sym-rec {R = R} S prel psym pprop r+ = go r+ where
-  go : ∀ {x y} → Sym R x y → S x y
-  go (symmetric r) = psym r
-  go [ r ] = prel r
-  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
-```
-
-If two elements $x$ and $y$ are related in the symmetric closure, then
-either $R x y$ or $R y x$ in the original relation.
-
-```agda
-sym-clo-rel
-  : ∀ {x y} → Sym R x y → ∥ (R x y) ⊎ (R y x) ∥
-sym-clo-rel {R = R} =
-  Sym-rec (λ x y → ∥ (R x y) ⊎ (R y x) ∥)
-    (λ r → inc (inl r))
-    (λ r → inc (inr r))
-    squash
-```
-
-If the original relation is reflexive, then so is the symmetric closure.
-
-```agda
-sym-clo-reflexive : is-reflexive R → is-reflexive (Sym R)
-sym-clo-reflexive is-refl x = [ is-refl x ]
-```
-
-Note that this is *not* true for transitivity! To see why, consider an
-irreflexive transitive relation on a type with at least related 2
-elements $R x y$ . If the symmetric closure of this relation was
-transitive, we'd be able to create a loop $R^{\leftrightarrow} x x$ in
-the symmetric closure by composing the relations $R^{\leftrightarrow} x
-y$ and $R^{\leftrightarrow} y x$.  However, if two elements are related
-in the symmetric closure, then they must be related in the original
-relation, which leads directly to a contradiction, as the original
-relation is irreflexive.
-
-For simplicity, we show this for the strict ordering on the natural
-numbers.
-
-```agda
-private
-  ¬sym-clo-transitive
-    : ¬ (is-transitive (Sym Nat._<_))
-  ¬sym-clo-transitive sym-clo-trans =
-    ∥-∥-rec! (⊎-rec (Nat.<-irrefl refl) (Nat.<-irrefl refl))
-      (sym-clo-rel (sym-clo-trans [ 0<1 ] (symmetric 0<1)))
-    where
-      0<1 : 0 Nat.< 1
-      0<1 = Nat.s≤s Nat.0≤x
-```
-
-As a corollary, we can see that the transitive closure of the symmetric closure
-is not the same as the symmetric closure of the transitive closure.
-
-However, the reflexive closure of the symmetric closure is equal to the
-symmetric closure of the reflexive closure.
-
-```agda
-sym-clo-refl-clo⊆refl-clo-sym-clo : Sym (Refl R) ⊆r Refl (Sym R)
-sym-clo-refl-clo⊆refl-clo-sym-clo {R = R} =
-  Sym-rec (Refl (Sym R))
-    (Refl-rec (Refl (Sym R))
-      (λ x~y → [ [ x~y ] ])
-      (λ _ → reflexive)
-      hlevel!)
-    (Refl-rec (flipr (Refl (Sym R)))
-      (λ y~x →  [ symmetric y~x ] )
-      (λ _ → reflexive)
-      hlevel!)
-    hlevel!
-
-refl-clo-sym-clo⊆sym-clo-refl-clo : Refl (Sym R) ⊆r Sym (Refl R)
-refl-clo-sym-clo⊆sym-clo-refl-clo {R = R} =
-  Refl-rec (Sym (Refl R))
-    (Sym-rec (Sym (Refl R))
-      (λ x~y → [ [ x~y ] ])
-      (λ x~y → symmetric [ x~y ])
-      hlevel!)
-    (λ _ → [ reflexive ])
-    hlevel!
-
-refl-clo-sym-clo≡sym-clo-refl-clo : Refl (Sym R) ≡ Sym (Refl R)
-refl-clo-sym-clo≡sym-clo-refl-clo =
-  prop-rel-ext trunc trunc
-    refl-clo-sym-clo⊆sym-clo-refl-clo
-    sym-clo-refl-clo⊆refl-clo-sym-clo
-```
-
-
-## Transitive Closure
-
-The transitive closure of a relation $R$ is the smallest transitive
-relation $R^{+}$ that contains $R$.
-
-```agda
-data Trans {A : Type ℓ} (_~_ : Rel A A ℓ') (x z : A) : Type (ℓ ⊔ ℓ') where
-  [_] : x ~ z → Trans _~_ x z
-  transitive : ∀ {y} → Trans _~_ x y → Trans _~_ y z → Trans _~_ x z
-  trunc : is-prop (Trans _~_ x z)
-```
-
-<!--
-```agda
-instance
-  Trans-H-Level : ∀ {x y} {n} → H-Level (Trans R x y) (suc n)
-  Trans-H-Level = prop-instance trunc
-
-Trans-elim
-  : (P : ∀ (x y : A) → Trans R x y → Type ℓ)
-  → (∀ {x y} → (r : R x y) → P x y [ r ])
-  → (∀ {x y z} → (r+ : Trans R x y) → (s+ : Trans R y z)
-     → P x y r+ → P y z s+
-     → P x z (transitive r+ s+))
-  → (∀ {x y} → (r+ : Trans R x y) → is-prop (P x y r+))
-  → ∀ {x y} → (r+ : Trans R x y) → P x y r+
-Trans-elim {R = R} P prel ptrans pprop r+ = go r+ where
-  go : ∀ {x y} → (r+ : Trans R x y) → P x y r+
-  go [ r ] = prel r
-  go (transitive r+ s+) = ptrans r+ s+ (go r+) (go s+)
-  go (trunc r+ r+' i) =
-    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
-```
--->
-
-The recursion principle for the transitive closure witnesses it's
-universal property; it is the smallest transitive relation containing $R$.
-
-```agda
-Trans-rec
-  : (S : A → A → Type ℓ)
-  → (∀ {x y} → (r : R x y) → S x y)
-  → (∀ {x y z} → S x y → S y z → S x z)
-  → (∀ {x y} → is-prop (S x y))
-  → ∀ {x y} → Trans R x y → S x y
-Trans-rec {R = R} S prel ptrans pprop r+ = go r+ where
-  go : ∀ {x y} → Trans R x y → S x y
-  go [ r ] = prel r
-  go (transitive r+ s+) = ptrans (go r+) (go s+)
-  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
-```
-
-If the original relation is reflexive or symmetric, then so is the
-transitive closure.
-
-```agda
-trans-clo-reflexive : is-reflexive R → is-reflexive (Trans R)
-trans-clo-reflexive is-refl x = [ is-refl x ]
-
-trans-clo-symmetric : is-symmetric R → is-symmetric (Trans R)
-trans-clo-symmetric {R = R} is-sym r+ =
-  Trans-rec (λ x y → Trans R y x)
-    (λ r → [ is-sym r ])
-    (λ r+ s+ → transitive s+ r+)
-    trunc
-    r+
-```
-
-## Reflexive-Transitive Closure
-
-The reflexive-transitive closure of a relation $R$ is the smallest
-reflexive and transitive relation $R^{*}$ that contains $R$.
-
-```agda
-data Refl-trans {A : Type ℓ} (R : A → A → Type ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where
-  [_] : ∀ {y} → R x y → Refl-trans R x y
-  reflexive : Refl-trans R x x
-  transitive : ∀ {y z} → Refl-trans R x y → Refl-trans R y z → Refl-trans R x z
-  trunc : ∀ {y} → is-prop (Refl-trans R x y)
-```
-
-<!--
-```agda
-instance
-  Refl-trans-H-Level : ∀ {x y} {n} → H-Level (Refl-trans R x y) (suc n)
-  Refl-trans-H-Level = prop-instance trunc
-
-Refl-trans-elim
-  : (P : ∀ (x y : A) → Refl-trans R x y → Type ℓ'')
-  → (∀ {x y} → (r : R x y) → P x y [ r ])
-  → (∀ {x} → P x x reflexive)
-  → (∀ {x y z} → (r+ : Refl-trans R x y) → (s+ : Refl-trans R y z)
-     → P x y r+ → P y z s+
-     → P x z (transitive r+ s+))
-  → (∀ {x y} → (r+ : Refl-trans R x y) → is-prop (P x y r+))
-  → ∀ {x y} → (r+ : Refl-trans R x y) → P x y r+
-Refl-trans-elim {R = R} P prel prefl ptrans pprop r+ = go r+ where
-  go : ∀ {x y} → (r+ : Refl-trans R x y) → P x y r+
-  go [ r ] = prel r
-  go reflexive = prefl
-  go (transitive r+ s+) = ptrans r+ s+ (go r+) (go s+)
-  go (trunc r+ r+' i) =
-    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
-```
--->
-
-Following the general theme, the recursion principle for the reflexive
-transitive closure witnesses it's universal property; it is the smallest
-reflexive and transitive relation containing $R$.
-
-```agda
-Refl-trans-rec
-  : (S : A → A → Type ℓ)
-  → (∀ {x y} → (r : R x y) → S x y)
-  → (∀ {x} → S x x)
-  → (∀ {x y z} → S x y → S y z → S x z)
-  → (∀ {x y} → is-prop (S x y))
-  → ∀ {x y} → Refl-trans R x y → S x y
-Refl-trans-rec {R = R} S prel prefl ptrans pprop r+ = go r+ where
-  go : ∀ {x y} → Refl-trans R x y → S x y
-  go [ r ] = prel r
-  go reflexive = prefl
-  go (transitive r+ s+) = ptrans (go r+) (go s+)
-  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
-```
-
-We also provide a recursion principle that inducts down the length of the
-chain of relations.
-
-```agda
-Refl-trans-rec-chain
-  : (S : A → A → Type ℓ)
-  → (∀ {x} → S x x)
-  → (∀ {x y z} → R x y → Refl-trans R y z → S y z → S x z)
-  → (∀ {x y} → is-prop (S x y))
-  → ∀ {x y} → Refl-trans R x y → S x y
-Refl-trans-rec-chain {R = R} S pnil pstep pprop r+ = go r+ reflexive pnil where
-  go : ∀ {x y z} → Refl-trans R x y → Refl-trans R y z → S y z → S x z
-  go [ x→y ] y→*z acc = pstep x→y y→*z acc
-  go reflexive y→*z acc = acc
-  go (transitive x→*x' x'→*y) y→*z acc =
-    go x→*x' (transitive x'→*y y→*z) (go x'→*y y→*z acc)
-  go (trunc x→*y x→*y' i) y→*z acc =
-    pprop (go x→*y y→*z acc) (go x→*y' y→*z acc) i
-```
-
-We also provide an eliminator for inspecting forks.
-
-```agda
-Refl-trans-case-fork
-  : (S : A → A → A → Type ℓ)
-  → (∀ {a y} → Refl-trans R' a y → S a a y)
-  → (∀ {a x} → Refl-trans R a x → S a x a)
-  → (∀ {a x y x' y'}
-     → R a x' → Refl-trans R x' x
-     → R' a y' → Refl-trans R' y' y
-     → S a x y)
-  → (∀ {a x y} → is-prop (S a x y))
-  → ∀ {a x y} → Refl-trans R a x → Refl-trans R' a y → S a x y
-Refl-trans-case-fork {R' = R'} {R = R} S refll reflr fork prop {a} {x} {y} a→*x a→*y =
-  Refl-trans-rec-chain (λ a x → Refl-trans R' a y → S a x y)
-    refll
-    (λ {a} {a'} {x} a→a' a'→*x _ a→*y →
-      Refl-trans-rec-chain
-        (λ a y → R a a' → Refl-trans R a' x → S a x y)
-        (λ a→a' a'→*x → reflr (transitive [ a→a' ] a'→*x))
-        (λ a→a' a'→*y _ a→a'' a''→*x → fork a→a'' a''→*x a→a' a'→*y)
-        (Π-is-hlevel 1 (λ _ → Π-is-hlevel 1 λ _ → prop))
-        a→*y a→a' a'→*x)
-    (Π-is-hlevel 1 (λ _ → prop))
-    a→*x a→*y
-```
-
-If the underlying relation is symmetric, then so is the
-reflexive-transitive closure.
-
-```agda
-refl-trans-clo-symmetric : is-symmetric R → is-symmetric (Refl-trans R)
-refl-trans-clo-symmetric {R = R} is-sym r+ =
-  Refl-trans-rec (λ x y → Refl-trans R y x)
-    (λ r → [ is-sym r ])
-    reflexive
-    (λ r+ s+ → transitive s+ r+)
-    trunc
-    r+
-```
-
-The reflexive closure and the transitive closure are contained in
-the reflexive transitive closure.
-
-```agda
-refl-clo⊆refl-trans-clo : Refl R ⊆r Refl-trans R
-refl-clo⊆refl-trans-clo {R = R} =
-  Refl-rec (Refl-trans R) [_] (λ _ → reflexive) hlevel!
-
-trans-clo⊆refl-trans-clo : Trans R ⊆r Refl-trans R
-trans-clo⊆refl-trans-clo {R = R} =
-  Trans-rec (Refl-trans R) [_] transitive hlevel!
-```
-
-
-Note that the reflexive-transitive closure is equivalent to taking
-the reflexive closure of the transitive closure.
-
-```agda
-refl-clo-trans-clo⊆refl-trans-clo : Refl (Trans R) ⊆r Refl-trans R
-refl-clo-trans-clo⊆refl-trans-clo {R = R} =
-  Refl-rec (Refl-trans R)
-    trans-clo⊆refl-trans-clo
-    (λ _ → reflexive)
-    hlevel!
-
-refl-trans-clo⊆refl-clo-trans-clo : Refl-trans R ⊆r Refl (Trans R)
-refl-trans-clo⊆refl-clo-trans-clo {R = R} =
-  Refl-trans-rec (Refl (Trans R))
-    (λ x~y → [ [ x~y ] ])
-    reflexive
-    (refl-clo-transitive transitive)
-    hlevel!
-
-refl-clo-trans-clo≡refl-trans-clo : Refl (Trans R) ≡ Refl-trans R
-refl-clo-trans-clo≡refl-trans-clo {R = R} =
-  prop-rel-ext trunc trunc
-    refl-clo-trans-clo⊆refl-trans-clo
-    refl-trans-clo⊆refl-clo-trans-clo
-```
-
-The same can be said for the transitive closure of the reflexive closure.
-
-```agda
-trans-clo-refl-clo⊆refl-trans-clo : Trans (Refl R) ⊆r Refl-trans R
-trans-clo-refl-clo⊆refl-trans-clo {R = R} =
-  Trans-rec (Refl-trans R)
-    refl-clo⊆refl-trans-clo
-    transitive
-    hlevel!
-
-refl-trans-clo⊆trans-clo-refl-clo : Refl-trans R ⊆r Trans (Refl R)
-refl-trans-clo⊆trans-clo-refl-clo {R = R} =
-  Refl-trans-rec (Trans (Refl R))
-    (λ x~y → [ [ x~y ] ])
-    [ reflexive ]
-    transitive
-    hlevel!
-
-trans-clo-refl-clo≡refl-trans-clo : Trans (Refl R) ≡ Refl-trans R
-trans-clo-refl-clo≡refl-trans-clo {R = R} =
-  prop-rel-ext trunc trunc
-    trans-clo-refl-clo⊆refl-trans-clo
-    refl-trans-clo⊆trans-clo-refl-clo
-```
-
-
-## Reflexive-Symmetric-Transitive Closure
-
-Finally, the reflexive-symmetric-transitive closure of a relation $R$ is
-the smallest reflexive, symmetric, and transitive relation
-$R^{\leftrightarrow*}$ that contains $R$.
-
-```agda
-data Refl-sym-trans {A : Type ℓ} (R : A → A → Type ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where
-  [_] : ∀ {y} → R x y → Refl-sym-trans R x y
-  reflexive : Refl-sym-trans R x x
-  symmetric : ∀ {y} → Refl-sym-trans R y x → Refl-sym-trans R x y
-  transitive : ∀ {y z} → Refl-sym-trans R x y → Refl-sym-trans R y z → Refl-sym-trans R x z
-  trunc : ∀ {y} → is-prop (Refl-sym-trans R x y)
-```
-
-<!--
-```agda
-instance
-  Refl-sym-trans-H-Level : ∀ {x y} {n} → H-Level (Refl-sym-trans R x y) (suc n)
-  Refl-sym-trans-H-Level = prop-instance trunc
-
-Refl-sym-trans-elim
-  : (P : ∀ (x y : A) → Refl-sym-trans R x y → Type ℓ'')
-  → (∀ {x y} → (r : R x y) → P x y [ r ])
-  → (∀ {x} → P x x reflexive)
-  → (∀ {x y} → (r+ : Refl-sym-trans R x y)
-     → P x y r+ → P y x (symmetric r+))
-  → (∀ {x y z} → (r+ : Refl-sym-trans R x y) → (s+ : Refl-sym-trans R y z)
-     → P x y r+ → P y z s+
-     → P x z (transitive r+ s+))
-  → (∀ {x y} → (r+ : Refl-sym-trans R x y) → is-prop (P x y r+))
-  → ∀ {x y} → (r+ : Refl-sym-trans R x y) → P x y r+
-Refl-sym-trans-elim {R = R} P prel prefl psym ptrans pprop r+ = go r+ where
-  go : ∀ {x y} → (r+ : Refl-sym-trans R x y) → P x y r+
-  go [ r ] = prel r
-  go reflexive = prefl
-  go (symmetric r) = psym r (go r)
-  go (transitive r+ s+) = ptrans r+ s+ (go r+) (go s+)
-  go (trunc r+ r+' i) =
-    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
-```
--->
-
-Yet again, the recursion principle for the reflexive, symmetric,
-transitive closure witnesses it's universal property; it is the smallest
-reflexive, symmetric, transitive relation containing $R$.
-
-```agda
-Refl-sym-trans-rec
-  : (S : A → A → Type ℓ)
-  → (∀ {x y} → (r : R x y) → S x y)
-  → (∀ {x} → S x x)
-  → (∀ {x y} → S x y → S y x)
-  → (∀ {x y z} → S x y → S y z → S x z)
-  → (∀ {x y} → is-prop (S x y))
-  → ∀ {x y} → Refl-sym-trans R x y → S x y
-Refl-sym-trans-rec {R = R} S prel prefl psym ptrans pprop r+ = go r+ where
-  go : ∀ {x y} → Refl-sym-trans R x y → S x y
-  go [ r ] = prel r
-  go reflexive = prefl
-  go (symmetric r) = psym (go r)
-  go (transitive r+ s+) = ptrans (go r+) (go s+)
-  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
-```
-
-We also define an alternative recursion principle for inducting down
-the length of the chain of relations.
-
-```agda
-Refl-sym-trans-rec-chain
-  : (S : A → A → Type ℓ)
-  → (∀ {x} → S x x)
-  → (∀ {x y z} → R x y → Refl-sym-trans R y z → S y z → S x z)
-  → (∀ {x y z} → R y x → Refl-sym-trans R y z → S y z → S x z)
-  → (∀ {x y} → is-prop (S x y))
-  → ∀ {x y} → Refl-sym-trans R x y → S x y
-Refl-sym-trans-rec-chain {R = R} S pnil pstep pinv pprop r+ = go r+ reflexive pnil where
-  go : ∀ {x y z} → Refl-sym-trans R x y → Refl-sym-trans R y z → S y z → S x z
-  go-sym : ∀ {x y z} → Refl-sym-trans R y x → Refl-sym-trans R y z → S y z → S x z
-
-  go [ x→y ] y→*z acc = pstep x→y y→*z acc
-  go reflexive y→*z acc = acc
-  go (symmetric y→*x) y→*z acc = go-sym y→*x y→*z acc
-  go (transitive x→*x' x'→*y) y→*z acc =
-    go x→*x' (transitive x'→*y y→*z) (go x'→*y y→*z acc)
-  go (trunc x→*y x→*y' i) y→*z acc =
-    pprop (go x→*y y→*z acc) (go x→*y' y→*z acc) i
-
-  go-sym [ y→x ] y→*z acc = pinv y→x y→*z acc
-  go-sym reflexive y→*z acc = acc
-  go-sym (symmetric x→*y) y→*z acc = go x→*y y→*z acc
-  go-sym (transitive y→*y' y'→*x) y→*z acc =
-    go-sym y'→*x (transitive (symmetric y→*y') y→*z) (go-sym y→*y' y→*z acc)
-  go-sym (trunc y→*x y→*x' i) y→*z acc =
-    pprop (go-sym y→*x y→*z acc) (go-sym y→*x' y→*z acc) i
-```
-
-The reflexive-transitive closure embeds into the reflexive symmetric
-transitive closure.
-
-```agda
-refl-trans⊆refl-sym-trans
-  : Refl-trans R ⊆r Refl-sym-trans R
-refl-trans⊆refl-sym-trans =
-  Refl-trans-rec (Refl-sym-trans _) [_] reflexive transitive trunc
-```
diff --git a/src/Data/Rel/Closure/Base.lagda.md b/src/Data/Rel/Closure/Base.lagda.md
new file mode 100644
index 000000000..885506280
--- /dev/null
+++ b/src/Data/Rel/Closure/Base.lagda.md
@@ -0,0 +1,80 @@
+<!--
+```agda
+open import 1Lab.Prelude
+open import Data.Sum
+
+open import Data.Rel.Base
+
+import Data.Nat as Nat
+import Data.Nat.Order as Nat
+```
+-->
+
+```agda
+module Data.Rel.Closure.Base where
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  R R' S : A → A → Type ℓ
+```
+-->
+
+# Closures of relations
+
+A **closure operator** $-^{+}$ on relations takes a relation $R$ on a type
+$A$ to a new relation $R^{+}$ on $A$, where $R^{+}$ is the smallest
+relation containing $R$ that satisfies some property.
+
+Intuitively, the closure of a relation should enjoy the following properties:
+- If $R \subseteq S$, then $R^{+} \subseteq S^{+}$.
+- $R \subseteq R^{+}$
+- $(R^{+})^{+} \subseteq R^{+}$, as closing $R$ under a property twice shouldn't
+  add any more elements.
+
+This ends up forming a [monad], though we do not define a closure operator as
+such due to annoying size restrictions.
+
+[monad]: Cat.Diagram.Monad.html
+
+```agda
+record is-rel-closure
+  (K : ∀ {ℓ ℓ'} {A : Type ℓ} → Rel A A ℓ' → Rel A A (ℓ ⊔ ℓ'))
+  : Typeω where
+  field
+    monotone : R ⊆r S → K R ⊆r K S
+    extensive : R ⊆r K R
+    closed : K (K R) ⊆r K R
+    has-prop : is-prop-rel (K R)
+```
+
+Closure, monotonicity, and extensivity combine to give idempotence
+of the closure operator.
+
+```agda
+  idempotent : K (K R) ≡ K R
+  idempotent =
+    prop-rel-ext has-prop has-prop
+      closed
+      (monotone extensive)
+```
+
+We can also derive an extension operator using the normal formulation
+for monads.
+
+```agda
+  extend : ∀ {R S : Rel A A ℓ} → S ⊆r K R → K S ⊆r K R
+  extend p kr = closed (monotone p kr)
+```
+
+We can leverage this to see that if $R \subseteq S \subseteq K R$, then
+$K R = K S$.
+
+```agda
+  ⊆+⊆-clo→≡ : ∀ {R S : Rel A A ℓ} → R ⊆r S → S ⊆r K R → K R ≡ K S
+  ⊆+⊆-clo→≡ p q =
+    prop-rel-ext has-prop has-prop (monotone p) (extend q)
+```
diff --git a/src/Data/Rel/Closure/Reflexive.lagda.md b/src/Data/Rel/Closure/Reflexive.lagda.md
new file mode 100644
index 000000000..aeb042332
--- /dev/null
+++ b/src/Data/Rel/Closure/Reflexive.lagda.md
@@ -0,0 +1,146 @@
+<!--
+```agda
+open import 1Lab.Prelude
+
+open import Data.Rel.Base
+open import Data.Rel.Closure.Base
+```
+-->
+
+```agda
+module Data.Rel.Closure.Reflexive where
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  R R' S : A → A → Type ℓ
+```
+-->
+
+# Reflexive Closure
+
+The reflexive [closure] of a [relation] $R$ is the smallest reflexive
+relation $R^{=}$ that contains $R$.
+
+[relation]: Data.Rel.Base.html
+[closure]: Data.Rel.Closure.html
+
+```agda
+data Refl {A : Type ℓ} (R : Rel A A ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where
+  reflexive : Refl R x x
+  [_] : ∀ {y} → R x y → Refl R x y
+  trunc : ∀ {y} → is-prop (Refl R x y)
+```
+
+<!--
+```agda
+instance
+  Refl-H-Level : ∀ {x y} {n} → H-Level (Refl R x y) (suc n)
+  Refl-H-Level = prop-instance trunc
+
+Refl-elim
+  : (P : ∀ (x y : A) → Refl R x y → Type ℓ'')
+  → (∀ {x y} → (r : R x y) → P x y [ r ])
+  → (∀ x → P x x reflexive)
+  → (∀ {x y} → (r+ : Refl R x y) → is-prop (P x y r+))
+  → ∀ {x y} → (r+ : Refl R x y) → P x y r+
+Refl-elim {R = R} P prel prefl pprop r+ = go r+ where
+  go : ∀ {x y} → (r+ : Refl R x y) → P x y r+
+  go reflexive = prefl _
+  go [ x ] = prel x
+  go (trunc r+ r+' i) =
+    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
+```
+-->
+
+The recursion principle for the reflexive closure of a relation witnesses
+the aforementioned universal property: it is the smallest reflexive
+relation containing $R$.
+
+```agda
+Refl-rec
+  : (S : A → A → Type ℓ)
+  → (∀ {x y} → R x y → S x y)
+  → (∀ x → S x x)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Refl R x y → S x y
+Refl-rec {R = R} S prel prefl pprop r+ = go r+ where
+  go : ∀ {x y} → Refl R x y → S x y
+  go reflexive = prefl _
+  go [ r ] = prel r
+  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
+```
+
+<!--
+```agda
+Refl-rec₂
+  : (S : A → A → A → Type ℓ)
+  → (∀ {x y z} → R x y → R' y z → S x y z)
+  → (∀ {x z} → R' x z → S x x z)
+  → (∀ {x y} → R x y → S x y y)
+  → (∀ x → S x x x)
+  → (∀ {x y z} → is-prop (S x y z))
+  → ∀ {x y z} → Refl R x y → Refl R' y z → S x y z
+Refl-rec₂ {R = R} {R' = R'} S prel prefll preflr prefl2 pprop r+ r+' = go r+ r+' where
+  go : ∀ {x y z} → Refl R x y → Refl R' y z → S x y z
+  go reflexive reflexive = prefl2 _
+  go reflexive [ r' ] = prefll r'
+  go reflexive (trunc r+ r+' i) =
+    pprop (go reflexive r+) (go reflexive r+') i
+  go [ r ] reflexive = preflr r
+  go [ r ] [ r' ] = prel r r'
+  go [ r ] (trunc r+ r+' i) =
+    pprop (go [ r ] r+) (go [ r ] r+') i
+  go (trunc r+ r+' i) r+'' =
+    pprop (go r+ r+'') (go r+' r+'') i
+```
+-->
+
+
+## As a closure operator
+
+As the name suggests, the reflexive closure of a relation forms a closure
+operator.
+
+```agda
+refl-clo-mono : R ⊆r S → Refl R ⊆r Refl S
+refl-clo-mono {S = S} p =
+  Refl-rec (Refl S) (λ r → [ p r ]) (λ _ → reflexive) trunc 
+
+refl-clo-closed : Refl (Refl R) ⊆r Refl R
+refl-clo-closed {R = R} = Refl-rec (Refl R) id (λ _ → reflexive) trunc
+
+refl-closure : is-rel-closure Refl
+refl-closure .is-rel-closure.monotone = refl-clo-mono
+refl-closure .is-rel-closure.extensive = [_]
+refl-closure .is-rel-closure.closed = refl-clo-closed
+refl-closure .is-rel-closure.has-prop = trunc
+```
+
+## Properties
+
+If the original relation is symmetric or transitive, then so is the
+reflexive closure.
+
+```agda
+refl-clo-symmetric
+  : is-symmetric R
+  → is-symmetric (Refl R)
+refl-clo-symmetric {R = R} is-sym =
+  Refl-rec (λ x y → Refl R y x)
+    (λ r → [ is-sym r ])
+    (λ _ → reflexive)
+    trunc
+
+refl-clo-transitive : is-transitive R → is-transitive (Refl R)
+refl-clo-transitive {R = R} is-trans =
+    Refl-rec₂ (λ x _ z → Refl R x z)
+      (λ x~*y y~*z → [ is-trans x~*y y~*z ])
+      [_]
+      [_]
+      (λ _ → reflexive)
+      trunc
+```
diff --git a/src/Data/Rel/Closure/ReflexiveSymmetricTransitive.lagda.md b/src/Data/Rel/Closure/ReflexiveSymmetricTransitive.lagda.md
new file mode 100644
index 000000000..a5507ee7a
--- /dev/null
+++ b/src/Data/Rel/Closure/ReflexiveSymmetricTransitive.lagda.md
@@ -0,0 +1,164 @@
+<!--
+```agda
+open import 1Lab.Prelude
+open import Data.Sum
+
+open import Data.Rel.Base
+open import Data.Rel.Closure.Base
+open import Data.Rel.Closure.Reflexive
+open import Data.Rel.Closure.Symmetric
+open import Data.Rel.Closure.Transitive
+open import Data.Rel.Closure.ReflexiveTransitive
+
+```
+-->
+
+```agda
+module Data.Rel.Closure.ReflexiveSymmetricTransitive where
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  R R' S : A → A → Type ℓ
+```
+-->
+
+# Reflexive-Symmetric-Transitive Closure
+
+Finally, the reflexive-symmetric-transitive closure of a relation $R$ is
+the smallest reflexive, symmetric, and transitive relation
+$R^{\leftrightarrow*}$ that contains $R$.
+
+```agda
+data Refl-sym-trans {A : Type ℓ} (R : A → A → Type ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where
+  [_] : ∀ {y} → R x y → Refl-sym-trans R x y
+  reflexive : Refl-sym-trans R x x
+  symmetric : ∀ {y} → Refl-sym-trans R y x → Refl-sym-trans R x y
+  transitive : ∀ {y z} → Refl-sym-trans R x y → Refl-sym-trans R y z → Refl-sym-trans R x z
+  trunc : ∀ {y} → is-prop (Refl-sym-trans R x y)
+```
+
+<!--
+```agda
+instance
+  Refl-sym-trans-H-Level : ∀ {x y} {n} → H-Level (Refl-sym-trans R x y) (suc n)
+  Refl-sym-trans-H-Level = prop-instance trunc
+
+Refl-sym-trans-elim
+  : (P : ∀ (x y : A) → Refl-sym-trans R x y → Type ℓ'')
+  → (∀ {x y} → (r : R x y) → P x y [ r ])
+  → (∀ {x} → P x x reflexive)
+  → (∀ {x y} → (r+ : Refl-sym-trans R x y)
+     → P x y r+ → P y x (symmetric r+))
+  → (∀ {x y z} → (r+ : Refl-sym-trans R x y) → (s+ : Refl-sym-trans R y z)
+     → P x y r+ → P y z s+
+     → P x z (transitive r+ s+))
+  → (∀ {x y} → (r+ : Refl-sym-trans R x y) → is-prop (P x y r+))
+  → ∀ {x y} → (r+ : Refl-sym-trans R x y) → P x y r+
+Refl-sym-trans-elim {R = R} P prel prefl psym ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → (r+ : Refl-sym-trans R x y) → P x y r+
+  go [ r ] = prel r
+  go reflexive = prefl
+  go (symmetric r) = psym r (go r)
+  go (transitive r+ s+) = ptrans r+ s+ (go r+) (go s+)
+  go (trunc r+ r+' i) =
+    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
+```
+-->
+
+Yet again, the recursion principle for the reflexive, symmetric,
+transitive closure witnesses it's universal property; it is the smallest
+reflexive, symmetric, transitive relation containing $R$.
+
+```agda
+Refl-sym-trans-rec
+  : (S : A → A → Type ℓ)
+  → (∀ {x y} → (r : R x y) → S x y)
+  → (∀ {x} → S x x)
+  → (∀ {x y} → S x y → S y x)
+  → (∀ {x y z} → S x y → S y z → S x z)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Refl-sym-trans R x y → S x y
+Refl-sym-trans-rec {R = R} S prel prefl psym ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → Refl-sym-trans R x y → S x y
+  go [ r ] = prel r
+  go reflexive = prefl
+  go (symmetric r) = psym (go r)
+  go (transitive r+ s+) = ptrans (go r+) (go s+)
+  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
+```
+
+We also define an alternative recursion principle for inducting down
+the length of the chain of relations.
+
+```agda
+Refl-sym-trans-rec-chain
+  : (S : A → A → Type ℓ)
+  → (∀ {x} → S x x)
+  → (∀ {x y z} → R x y → Refl-sym-trans R y z → S y z → S x z)
+  → (∀ {x y z} → R y x → Refl-sym-trans R y z → S y z → S x z)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Refl-sym-trans R x y → S x y
+Refl-sym-trans-rec-chain {R = R} S pnil pstep pinv pprop r+ = go r+ reflexive pnil where
+  go : ∀ {x y z} → Refl-sym-trans R x y → Refl-sym-trans R y z → S y z → S x z
+  go-sym : ∀ {x y z} → Refl-sym-trans R y x → Refl-sym-trans R y z → S y z → S x z
+
+  go [ x→y ] y→*z acc = pstep x→y y→*z acc
+  go reflexive y→*z acc = acc
+  go (symmetric y→*x) y→*z acc = go-sym y→*x y→*z acc
+  go (transitive x→*x' x'→*y) y→*z acc =
+    go x→*x' (transitive x'→*y y→*z) (go x'→*y y→*z acc)
+  go (trunc x→*y x→*y' i) y→*z acc =
+    pprop (go x→*y y→*z acc) (go x→*y' y→*z acc) i
+
+  go-sym [ y→x ] y→*z acc = pinv y→x y→*z acc
+  go-sym reflexive y→*z acc = acc
+  go-sym (symmetric x→*y) y→*z acc = go x→*y y→*z acc
+  go-sym (transitive y→*y' y'→*x) y→*z acc =
+    go-sym y'→*x (transitive (symmetric y→*y') y→*z) (go-sym y→*y' y→*z acc)
+  go-sym (trunc y→*x y→*x' i) y→*z acc =
+    pprop (go-sym y→*x y→*z acc) (go-sym y→*x' y→*z acc) i
+```
+
+## As a closure operator
+
+```agda
+refl-sym-trans-clo-mono : R ⊆r S → Refl-sym-trans R ⊆r Refl-sym-trans S
+refl-sym-trans-clo-mono {S = S} p =
+  Refl-sym-trans-rec (Refl-sym-trans S)
+      (λ r → [ p r ])
+      reflexive
+      symmetric
+      transitive
+      trunc
+
+refl-sym-trans-clo-closed : Refl-sym-trans (Refl-sym-trans R) ⊆r Refl-sym-trans R
+refl-sym-trans-clo-closed {R = R} =
+  Refl-sym-trans-rec (Refl-sym-trans R)
+    id
+    reflexive
+    symmetric
+    transitive
+    trunc
+
+refl-sym-trans-closure : is-rel-closure Refl-sym-trans
+refl-sym-trans-closure .is-rel-closure.monotone = refl-sym-trans-clo-mono
+refl-sym-trans-closure .is-rel-closure.extensive = [_]
+refl-sym-trans-closure .is-rel-closure.closed = refl-sym-trans-clo-closed
+refl-sym-trans-closure .is-rel-closure.has-prop = trunc
+```
+
+## Properties
+
+The reflexive-transitive closure embeds into the reflexive symmetric
+transitive closure.
+
+```agda
+refl-trans⊆refl-sym-trans
+  : Refl-trans R ⊆r Refl-sym-trans R
+refl-trans⊆refl-sym-trans =
+  Refl-trans-rec (Refl-sym-trans _) [_] reflexive transitive trunc
+```
diff --git a/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
new file mode 100644
index 000000000..531b2bfc4
--- /dev/null
+++ b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
@@ -0,0 +1,212 @@
+<!--
+```agda
+open import 1Lab.Prelude
+open import Data.Sum
+
+open import Data.Rel.Base
+open import Data.Rel.Closure.Base
+open import Data.Rel.Closure.Reflexive
+open import Data.Rel.Closure.Transitive
+
+```
+-->
+
+```agda
+module Data.Rel.Closure.ReflexiveTransitive where
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  R R' S : A → A → Type ℓ
+```
+-->
+
+# Reflexive-Transitive Closure
+
+The reflexive-transitive [closure] of a [relation] $R$ is the smallest
+reflexive and transitive relation $R^{*}$ that contains $R$.
+
+[relation]: Data.Rel.Base.html
+[closure]: Data.Rel.Closure.html
+
+```agda
+data Refl-trans {A : Type ℓ} (R : A → A → Type ℓ') (x : A) : A → Type (ℓ ⊔ ℓ') where
+  [_] : ∀ {y} → R x y → Refl-trans R x y
+  reflexive : Refl-trans R x x
+  transitive : ∀ {y z} → Refl-trans R x y → Refl-trans R y z → Refl-trans R x z
+  trunc : ∀ {y} → is-prop (Refl-trans R x y)
+```
+
+<!--
+```agda
+instance
+  Refl-trans-H-Level : ∀ {x y} {n} → H-Level (Refl-trans R x y) (suc n)
+  Refl-trans-H-Level = prop-instance trunc
+
+Refl-trans-elim
+  : (P : ∀ (x y : A) → Refl-trans R x y → Type ℓ'')
+  → (∀ {x y} → (r : R x y) → P x y [ r ])
+  → (∀ {x} → P x x reflexive)
+  → (∀ {x y z} → (r+ : Refl-trans R x y) → (s+ : Refl-trans R y z)
+     → P x y r+ → P y z s+
+     → P x z (transitive r+ s+))
+  → (∀ {x y} → (r+ : Refl-trans R x y) → is-prop (P x y r+))
+  → ∀ {x y} → (r+ : Refl-trans R x y) → P x y r+
+Refl-trans-elim {R = R} P prel prefl ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → (r+ : Refl-trans R x y) → P x y r+
+  go [ r ] = prel r
+  go reflexive = prefl
+  go (transitive r+ s+) = ptrans r+ s+ (go r+) (go s+)
+  go (trunc r+ r+' i) =
+    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
+```
+-->
+
+Following the general theme, the recursion principle for the reflexive
+transitive closure witnesses it's universal property; it is the smallest
+reflexive and transitive relation containing $R$.
+
+```agda
+Refl-trans-rec
+  : (S : A → A → Type ℓ)
+  → (∀ {x y} → (r : R x y) → S x y)
+  → (∀ {x} → S x x)
+  → (∀ {x y z} → S x y → S y z → S x z)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Refl-trans R x y → S x y
+Refl-trans-rec {R = R} S prel prefl ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → Refl-trans R x y → S x y
+  go [ r ] = prel r
+  go reflexive = prefl
+  go (transitive r+ s+) = ptrans (go r+) (go s+)
+  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
+```
+
+We also provide a recursion principle that inducts down the length of the
+chain of relations.
+
+```agda
+Refl-trans-rec-chain
+  : (S : A → A → Type ℓ)
+  → (∀ {x} → S x x)
+  → (∀ {x y z} → R x y → Refl-trans R y z → S y z → S x z)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Refl-trans R x y → S x y
+Refl-trans-rec-chain {R = R} S pnil pstep pprop r+ = go r+ reflexive pnil where
+  go : ∀ {x y z} → Refl-trans R x y → Refl-trans R y z → S y z → S x z
+  go [ x→y ] y→*z acc = pstep x→y y→*z acc
+  go reflexive y→*z acc = acc
+  go (transitive x→*x' x'→*y) y→*z acc =
+    go x→*x' (transitive x'→*y y→*z) (go x'→*y y→*z acc)
+  go (trunc x→*y x→*y' i) y→*z acc =
+    pprop (go x→*y y→*z acc) (go x→*y' y→*z acc) i
+```
+
+We also provide an eliminator for inspecting forks.
+
+```agda
+Refl-trans-case-fork
+  : (S : A → A → A → Type ℓ)
+  → (∀ {a y} → Refl-trans R' a y → S a a y)
+  → (∀ {a x} → Refl-trans R a x → S a x a)
+  → (∀ {a x y x' y'}
+     → R a x' → Refl-trans R x' x
+     → R' a y' → Refl-trans R' y' y
+     → S a x y)
+  → (∀ {a x y} → is-prop (S a x y))
+  → ∀ {a x y} → Refl-trans R a x → Refl-trans R' a y → S a x y
+Refl-trans-case-fork {R' = R'} {R = R} S refll reflr fork prop {a} {x} {y} a→*x a→*y =
+  Refl-trans-rec-chain (λ a x → Refl-trans R' a y → S a x y)
+    refll
+    (λ {a} {a'} {x} a→a' a'→*x _ a→*y →
+      Refl-trans-rec-chain
+        (λ a y → R a a' → Refl-trans R a' x → S a x y)
+        (λ a→a' a'→*x → reflr (transitive [ a→a' ] a'→*x))
+        (λ a→a' a'→*y _ a→a'' a''→*x → fork a→a'' a''→*x a→a' a'→*y)
+        (Π-is-hlevel 1 (λ _ → Π-is-hlevel 1 λ _ → prop))
+        a→*y a→a' a'→*x)
+    (Π-is-hlevel 1 (λ _ → prop))
+    a→*x a→*y
+```
+
+If the underlying relation is symmetric, then so is the
+reflexive-transitive closure.
+
+```agda
+refl-trans-clo-symmetric : is-symmetric R → is-symmetric (Refl-trans R)
+refl-trans-clo-symmetric {R = R} is-sym r+ =
+  Refl-trans-rec (λ x y → Refl-trans R y x)
+    (λ r → [ is-sym r ])
+    reflexive
+    (λ r+ s+ → transitive s+ r+)
+    trunc
+    r+
+```
+
+The reflexive closure and the transitive closure are contained in
+the reflexive transitive closure.
+
+```agda
+refl-clo⊆refl-trans-clo : Refl R ⊆r Refl-trans R
+refl-clo⊆refl-trans-clo {R = R} =
+  Refl-rec (Refl-trans R) [_] (λ _ → reflexive) hlevel!
+
+trans-clo⊆refl-trans-clo : Trans R ⊆r Refl-trans R
+trans-clo⊆refl-trans-clo {R = R} =
+  Trans-rec (Refl-trans R) [_] transitive hlevel!
+```
+
+
+Note that the reflexive-transitive closure is equivalent to taking
+the reflexive closure of the transitive closure.
+
+```agda
+refl-clo-trans-clo⊆refl-trans-clo : Refl (Trans R) ⊆r Refl-trans R
+refl-clo-trans-clo⊆refl-trans-clo {R = R} =
+  Refl-rec (Refl-trans R)
+    trans-clo⊆refl-trans-clo
+    (λ _ → reflexive)
+    hlevel!
+
+refl-trans-clo⊆refl-clo-trans-clo : Refl-trans R ⊆r Refl (Trans R)
+refl-trans-clo⊆refl-clo-trans-clo {R = R} =
+  Refl-trans-rec (Refl (Trans R))
+    (λ x~y → [ [ x~y ] ])
+    reflexive
+    (refl-clo-transitive transitive)
+    hlevel!
+
+refl-clo-trans-clo≡refl-trans-clo : Refl (Trans R) ≡ Refl-trans R
+refl-clo-trans-clo≡refl-trans-clo {R = R} =
+  prop-rel-ext trunc trunc
+    refl-clo-trans-clo⊆refl-trans-clo
+    refl-trans-clo⊆refl-clo-trans-clo
+```
+
+The same can be said for the transitive closure of the reflexive closure.
+
+```agda
+trans-clo-refl-clo⊆refl-trans-clo : Trans (Refl R) ⊆r Refl-trans R
+trans-clo-refl-clo⊆refl-trans-clo {R = R} =
+  Trans-rec (Refl-trans R)
+    refl-clo⊆refl-trans-clo
+    transitive
+    hlevel!
+
+refl-trans-clo⊆trans-clo-refl-clo : Refl-trans R ⊆r Trans (Refl R)
+refl-trans-clo⊆trans-clo-refl-clo {R = R} =
+  Refl-trans-rec (Trans (Refl R))
+    (λ x~y → [ [ x~y ] ])
+    [ reflexive ]
+    transitive
+    hlevel!
+
+trans-clo-refl-clo≡refl-trans-clo : Trans (Refl R) ≡ Refl-trans R
+trans-clo-refl-clo≡refl-trans-clo {R = R} =
+  prop-rel-ext trunc trunc
+    trans-clo-refl-clo⊆refl-trans-clo
+    refl-trans-clo⊆trans-clo-refl-clo
+```
diff --git a/src/Data/Rel/Closure/Symmetric.lagda.md b/src/Data/Rel/Closure/Symmetric.lagda.md
new file mode 100644
index 000000000..e6fa10a36
--- /dev/null
+++ b/src/Data/Rel/Closure/Symmetric.lagda.md
@@ -0,0 +1,189 @@
+<!--
+```agda
+open import 1Lab.Prelude
+open import Data.Sum
+
+open import Data.Rel.Base
+open import Data.Rel.Closure.Base
+open import Data.Rel.Closure.Reflexive
+
+import Data.Nat as Nat
+import Data.Nat.Order as Nat
+```
+-->
+
+
+```agda
+module Data.Rel.Closure.Symmetric where
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  R R' S : A → A → Type ℓ
+```
+-->
+
+# Symmetric Closure
+
+The symmetric [closure] of a [relation] $R$ is the smallest symmetric
+relation $R^{\leftrightarrow}$ that contains $R$.
+
+[closure]: Data.Rel.Closure.html
+[relation]: Data.Rel.Base.html
+
+```agda
+data Sym {A : Type ℓ} (R : A → A → Type ℓ') (x y : A) : Type (ℓ ⊔ ℓ') where
+  symmetric : Sym R y x → Sym R x y
+  [_] : R x y → Sym R x y
+  trunc : is-prop (Sym R x y)
+```
+
+<!--
+```agda
+instance
+  Sym-H-Level : ∀ {x y} {n} → H-Level (Sym R x y) (suc n)
+  Sym-H-Level = prop-instance trunc
+
+Sym-elim
+  : (P : ∀ (x y : A) → Sym R x y → Type ℓ'')
+  → (∀ {x y} → (r : R x y) → P x y [ r ])
+  → (∀ {x y} → (r : Sym R y x) → P x y (symmetric r))
+  → (∀ {x y} → (r+ : Sym R x y) → is-prop (P x y r+))
+  → ∀ {x y} → (r+ : Sym R x y) → P x y r+
+Sym-elim {R = R} P prel psym pprop r+ = go r+ where
+  go : ∀ {x y} → (r+ : Sym R x y) → P x y r+
+  go (symmetric x) = psym x
+  go [ x ] = prel x
+  go (trunc r+ r+' i) =
+    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
+```
+-->
+
+Like the [reflexive closure], the recursion principle for the symmetric
+closure witnesses it's universal property; it is the smallest symmetric
+relation containing $R$.
+
+[reflexive closure]: Data.Rel.Closure.Reflexive.html
+
+```agda
+Sym-rec
+  : (S : A → A → Type ℓ)
+  → (∀ {x y} → R x y → S x y)
+  → (∀ {x y} → S x y → S y x)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Sym R x y → S x y
+Sym-rec {R = R} S prel psym pprop r+ = go r+ where
+  go : ∀ {x y} → Sym R x y → S x y
+  go (symmetric r) = psym (go r)
+  go [ r ] = prel r
+  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
+```
+
+## As a closure operator
+
+It is straightforward to show that the symmetric closure is a closure
+operator.
+
+```agda
+sym-clo-mono : R ⊆r S → Sym R ⊆r Sym S
+sym-clo-mono {S = S} p =
+  Sym-rec (Sym S) (λ r → [ p r ]) symmetric trunc
+
+sym-clo-closed : Sym (Sym R) ⊆r Sym R
+sym-clo-closed {R = R} =
+  Sym-rec (Sym R) id symmetric trunc
+
+sym-closure : is-rel-closure Sym
+sym-closure .is-rel-closure.monotone = sym-clo-mono
+sym-closure .is-rel-closure.extensive = [_]
+sym-closure .is-rel-closure.closed = sym-clo-closed
+sym-closure .is-rel-closure.has-prop = trunc
+```
+
+
+## Properties
+
+If two elements $x$ and $y$ are related in the symmetric closure, then
+either $R x y$ or $R y x$ in the original relation.
+
+```agda
+sym-clo-rel
+  : ∀ {x y} → Sym R x y → ∥ (R x y) ⊎ (R y x) ∥
+sym-clo-rel {R = R} =
+  Sym-rec (λ x y → ∥ (R x y) ⊎ (R y x) ∥)
+    (λ r → inc (inl r))
+    (∥-∥-map (⊎-rec inr inl))
+    squash
+```
+
+If the original relation is reflexive, then so is the symmetric closure.
+
+```agda
+sym-clo-reflexive : is-reflexive R → is-reflexive (Sym R)
+sym-clo-reflexive is-refl x = [ is-refl x ]
+```
+
+Note that this is *not* true for transitivity! To see why, consider an
+irreflexive transitive relation on a type with at least related 2
+elements $R x y$ . If the symmetric closure of this relation was
+transitive, we'd be able to create a loop $R^{\leftrightarrow} x x$ in
+the symmetric closure by composing the relations $R^{\leftrightarrow} x
+y$ and $R^{\leftrightarrow} y x$.  However, if two elements are related
+in the symmetric closure, then they must be related in the original
+relation, which leads directly to a contradiction, as the original
+relation is irreflexive.
+
+For simplicity, we show this for the strict ordering on the natural
+numbers.
+
+```agda
+private
+  ¬sym-clo-transitive
+    : ¬ (is-transitive (Sym Nat._<_))
+  ¬sym-clo-transitive sym-clo-trans =
+    ∥-∥-rec! (⊎-rec (Nat.<-irrefl refl) (Nat.<-irrefl refl))
+      (sym-clo-rel (sym-clo-trans [ 0<1 ] (symmetric [ 0<1 ])))
+    where
+      0<1 : 0 Nat.< 1
+      0<1 = Nat.s≤s Nat.0≤x
+```
+
+As a corollary, we can see that the transitive closure of the symmetric closure
+is not the same as the symmetric closure of the transitive closure.
+
+However, the reflexive closure of the symmetric closure is equal to the
+symmetric closure of the reflexive closure.
+
+```agda
+sym-clo-refl-clo⊆refl-clo-sym-clo : Sym (Refl R) ⊆r Refl (Sym R)
+sym-clo-refl-clo⊆refl-clo-sym-clo {R = R} =
+  Sym-rec (Refl (Sym R))
+    (Refl-rec (Refl (Sym R))
+      (λ x~y → [ [ x~y ] ])
+      (λ _ → reflexive)
+      hlevel!)
+    (Refl-rec (flipr (Refl (Sym R)))
+      (λ y~x →  [ symmetric y~x ] )
+      (λ _ → reflexive)
+      hlevel!)
+    hlevel!
+
+refl-clo-sym-clo⊆sym-clo-refl-clo : Refl (Sym R) ⊆r Sym (Refl R)
+refl-clo-sym-clo⊆sym-clo-refl-clo {R = R} =
+  Refl-rec (Sym (Refl R))
+    (Sym-rec (Sym (Refl R))
+      (λ x~y → [ [ x~y ] ])
+      symmetric
+      hlevel!)
+    (λ _ → [ reflexive ])
+    hlevel!
+
+refl-clo-sym-clo≡sym-clo-refl-clo : Refl (Sym R) ≡ Sym (Refl R)
+refl-clo-sym-clo≡sym-clo-refl-clo =
+  prop-rel-ext trunc trunc
+    refl-clo-sym-clo⊆sym-clo-refl-clo
+    sym-clo-refl-clo⊆refl-clo-sym-clo
+```
diff --git a/src/Data/Rel/Closure/Transitive.lagda.md b/src/Data/Rel/Closure/Transitive.lagda.md
new file mode 100644
index 000000000..2b1f52c80
--- /dev/null
+++ b/src/Data/Rel/Closure/Transitive.lagda.md
@@ -0,0 +1,113 @@
+<!--
+```agda
+open import 1Lab.Prelude
+open import Data.Sum
+
+open import Data.Rel.Base
+open import Data.Rel.Closure.Base
+```
+-->
+
+```agda
+module Data.Rel.Closure.Transitive where
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  R R' S : A → A → Type ℓ
+```
+-->
+
+# Transitive Closure
+
+The transitive [closure] of a [relation] $R$ is the smallest transitive
+relation $R^{+}$ that contains $R$.
+
+[relation]: Data.Rel.Base.html
+[closure]: Data.Rel.Closure.html
+
+```agda
+data Trans {A : Type ℓ} (_~_ : Rel A A ℓ') (x z : A) : Type (ℓ ⊔ ℓ') where
+  [_] : x ~ z → Trans _~_ x z
+  transitive : ∀ {y} → Trans _~_ x y → Trans _~_ y z → Trans _~_ x z
+  trunc : is-prop (Trans _~_ x z)
+```
+
+<!--
+```agda
+instance
+  Trans-H-Level : ∀ {x y} {n} → H-Level (Trans R x y) (suc n)
+  Trans-H-Level = prop-instance trunc
+
+Trans-elim
+  : (P : ∀ (x y : A) → Trans R x y → Type ℓ)
+  → (∀ {x y} → (r : R x y) → P x y [ r ])
+  → (∀ {x y z} → (r+ : Trans R x y) → (s+ : Trans R y z)
+     → P x y r+ → P y z s+
+     → P x z (transitive r+ s+))
+  → (∀ {x y} → (r+ : Trans R x y) → is-prop (P x y r+))
+  → ∀ {x y} → (r+ : Trans R x y) → P x y r+
+Trans-elim {R = R} P prel ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → (r+ : Trans R x y) → P x y r+
+  go [ r ] = prel r
+  go (transitive r+ s+) = ptrans r+ s+ (go r+) (go s+)
+  go (trunc r+ r+' i) =
+    is-prop→pathp (λ i → pprop (trunc r+ r+' i)) (go r+) (go r+') i
+```
+-->
+
+The recursion principle for the transitive closure witnesses it's
+universal property; it is the smallest transitive relation containing $R$.
+
+```agda
+Trans-rec
+  : (S : A → A → Type ℓ)
+  → (∀ {x y} → (r : R x y) → S x y)
+  → (∀ {x y z} → S x y → S y z → S x z)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Trans R x y → S x y
+Trans-rec {R = R} S prel ptrans pprop r+ = go r+ where
+  go : ∀ {x y} → Trans R x y → S x y
+  go [ r ] = prel r
+  go (transitive r+ s+) = ptrans (go r+) (go s+)
+  go (trunc r+ r+' i) = pprop (go r+) (go r+') i
+```
+
+## As a closure operator
+
+```agda
+trans-clo-mono : R ⊆r S → Trans R ⊆r Trans S
+trans-clo-mono {S = S} p =
+  Trans-rec (Trans S) (λ r → [ p r ]) transitive trunc
+
+trans-clo-closed : Trans (Trans R) ⊆r Trans R
+trans-clo-closed {R = R} =
+  Trans-rec (Trans R) id transitive trunc
+
+trans-closure : is-rel-closure Trans
+trans-closure .is-rel-closure.monotone = trans-clo-mono
+trans-closure .is-rel-closure.extensive = [_]
+trans-closure .is-rel-closure.closed = trans-clo-closed
+trans-closure .is-rel-closure.has-prop = trunc
+```
+
+## Properties
+
+If the original relation is reflexive or symmetric, then so is the
+transitive closure.
+
+```agda
+trans-clo-reflexive : is-reflexive R → is-reflexive (Trans R)
+trans-clo-reflexive is-refl x = [ is-refl x ]
+
+trans-clo-symmetric : is-symmetric R → is-symmetric (Trans R)
+trans-clo-symmetric {R = R} is-sym r+ =
+  Trans-rec (λ x y → Trans R y x)
+    (λ r → [ is-sym r ])
+    (λ r+ s+ → transitive s+ r+)
+    trunc
+    r+
+```

From 3627ec079242a5cc59750a68bb6eefbd1b47fbe1 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Tue, 27 Jun 2023 11:09:15 -0700
Subject: [PATCH 11/19] def: write prose for commuting rewrites

---
 src/Data/Rel/Base.lagda.md                    |   3 +
 src/Data/Rel/Closure/Base.lagda.md            |   8 +-
 .../Rel/Closure/ReflexiveTransitive.lagda.md  |  29 ++
 src/Rewriting/Base.lagda.md                   | 104 +++++
 src/Rewriting/Commute.lagda.md                | 362 ++++++++++++++++++
 5 files changed, 502 insertions(+), 4 deletions(-)
 create mode 100644 src/Rewriting/Base.lagda.md
 create mode 100644 src/Rewriting/Commute.lagda.md

diff --git a/src/Data/Rel/Base.lagda.md b/src/Data/Rel/Base.lagda.md
index 5c0ddeeb8..561c111e1 100644
--- a/src/Data/Rel/Base.lagda.md
+++ b/src/Data/Rel/Base.lagda.md
@@ -79,6 +79,9 @@ if $R(x,y)$ implies $S(x,y)$ for every $x$ and $y$.
 ```agda
 _⊆r_ : Rel A B ℓ → Rel A B ℓ' → Type _
 R ⊆r S = ∀ {x y} → R x y → S x y
+
+_≃r_ : Rel A B ℓ → Rel A B ℓ' → Type _
+R ≃r S = ∀ {x y} → R x y ≃ S x y
 ```
 
 ```agda
diff --git a/src/Data/Rel/Closure/Base.lagda.md b/src/Data/Rel/Closure/Base.lagda.md
index 885506280..7079261a8 100644
--- a/src/Data/Rel/Closure/Base.lagda.md
+++ b/src/Data/Rel/Closure/Base.lagda.md
@@ -66,7 +66,7 @@ We can also derive an extension operator using the normal formulation
 for monads.
 
 ```agda
-  extend : ∀ {R S : Rel A A ℓ} → S ⊆r K R → K S ⊆r K R
+  extend : S ⊆r K R → K S ⊆r K R
   extend p kr = closed (monotone p kr)
 ```
 
@@ -74,7 +74,7 @@ We can leverage this to see that if $R \subseteq S \subseteq K R$, then
 $K R = K S$.
 
 ```agda
-  ⊆+⊆-clo→≡ : ∀ {R S : Rel A A ℓ} → R ⊆r S → S ⊆r K R → K R ≡ K S
-  ⊆+⊆-clo→≡ p q =
-    prop-rel-ext has-prop has-prop (monotone p) (extend q)
+  ⊆+⊆-clo→≃ : S ⊆r R → R ⊆r K S → K R ≃r K S
+  ⊆+⊆-clo→≃ p q =
+    prop-ext has-prop has-prop  (extend q) (monotone p)
 ```
diff --git a/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
index 531b2bfc4..e49aab30c 100644
--- a/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
+++ b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
@@ -132,6 +132,35 @@ Refl-trans-case-fork {R' = R'} {R = R} S refll reflr fork prop {a} {x} {y} a→*
     a→*x a→*y
 ```
 
+## As a closure operator
+
+```agda
+refl-trans-clo-mono : R ⊆r S → Refl-trans R ⊆r Refl-trans S
+refl-trans-clo-mono {S = S} p =
+  Refl-trans-rec (Refl-trans S)
+      (λ r → [ p r ])
+      reflexive
+      transitive
+      trunc
+
+refl-trans-clo-closed : Refl-trans (Refl-trans R) ⊆r Refl-trans R
+refl-trans-clo-closed {R = R} =
+  Refl-trans-rec (Refl-trans R)
+    id
+    reflexive
+    transitive
+    trunc
+
+refl-trans-closure : is-rel-closure Refl-trans
+refl-trans-closure .is-rel-closure.monotone = refl-trans-clo-mono
+refl-trans-closure .is-rel-closure.extensive = [_]
+refl-trans-closure .is-rel-closure.closed = refl-trans-clo-closed
+refl-trans-closure .is-rel-closure.has-prop = trunc
+```
+
+
+## Properties
+
 If the underlying relation is symmetric, then so is the
 reflexive-transitive closure.
 
diff --git a/src/Rewriting/Base.lagda.md b/src/Rewriting/Base.lagda.md
new file mode 100644
index 000000000..aa26843b0
--- /dev/null
+++ b/src/Rewriting/Base.lagda.md
@@ -0,0 +1,104 @@
+<!--
+```agda
+open import 1Lab.Prelude
+open import Data.Rel.Base
+open import Data.Rel.Closure
+```
+-->
+
+```agda
+module Rewriting.Base where
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  R S _↝₁_ _↝₂_ : Rel A A ℓ
+```
+-->
+
+# Abstract Rewriting Systems
+
+Many problems in computer science can be phrased in terms of
+**term rewriting systems**. Concretely, these are given by a collection
+of terms in some language, along with a collection of rules that describe
+how we can simplify terms. As an example, the untyped $\lambda$-calculus
+can be naturally presented as a term rewriting system, where only
+reduction rule is $\beta$-reduction. More abstractly, a rewriting system
+on a type $A$ is simply a [relation] $\to$ on $A$ which encodes the
+rewriting rules. Sequences of rewrites are then described using the
+[reflexive transitive closure] of $\to$.
+
+[relation]: Data.Rel.Base.html
+[reflexive transitive closure]: Data.Rel.Closure.html#reflexive-transitive-closure.html
+
+## Basic Concepts
+
+Let $R$ and $S$ be a pair of relations on $A$. We say that
+2 elements $x$ and $y$ are **joinable** by $R$ and $S$ if there
+exists some $z$ such that $R(x,z)$ and $S(y,z)$.
+
+```agda
+is-joinable 
+  : ∀ {ℓa ℓr ℓs} {A : Type ℓa}
+  → (R : Rel A A ℓr) (S : Rel A A ℓs)
+  → A → A → Type _
+is-joinable {A = A} R S x y = ∃[ z ∈ A ] (R x z × S y z)
+```
+
+This is equivalent to the composite of $S^{-1}$ and $R$, but this is
+less intuitive to think about.
+
+```agda
+private
+  ∘≡joinable
+    : ∀ {R : Rel A A ℓ} {S : Rel A A ℓ'} {x y : A}
+    → (flipr S ∘r R) x y ≡ is-joinable R S x y
+  ∘≡joinable = refl
+```
+
+Let $P$, $Q$, $R$ and $S$ all be relations on $A$. We say that $P$ and
+$Q$ are resolvable by $R$ and $S$ if for all $x,y,z : A$, $P(x,y)$ and
+$Q(x,z)$ implies that $y$ and $z$ are joinable by $R$ and $S$.
+
+~~~{.quiver}
+\begin{tikzcd}
+  & x \\
+  y && z \\
+  & {\exists! w}
+  \arrow["R"', dashed, from=2-1, to=3-2]
+  \arrow["S", dashed, from=2-3, to=3-2]
+  \arrow["P"', from=1-2, to=2-1]
+  \arrow["Q", from=1-2, to=2-3]
+\end{tikzcd}
+~~~
+
+```agda
+is-resolvable
+  : ∀ {ℓa ℓp ℓq ℓr ℓs} {A : Type ℓa}
+  → (P : Rel A A ℓp) → (Q : Rel A A ℓq)
+  → (R : Rel A A ℓr) → (S : Rel A A ℓs)
+  → Type _
+is-resolvable {A = A} P Q R S =
+  ∀ {x y z} → P x y → Q x z → is-joinable R S y z
+```
+
+This condition is equivalent to $Q \circ P^{-1} \subseteq S^{-1} \circ R$,
+but the latter version is much more confusing to think about.
+
+```agda
+private
+  ←∘→⊆→∘←≃resolvable
+    : ∀ {ℓa ℓp ℓq ℓr ℓs} {A : Type ℓa}
+    → {P : Rel A A ℓp} {Q : Rel A A ℓq}
+    → {R : Rel A A ℓr} {S : Rel A A ℓs}
+    → ((Q ∘r flipr P) ⊆r (flipr S ∘r R)) ≃ is-resolvable P Q R S
+  ←∘→⊆→∘←≃resolvable =
+    prop-ext!
+      (λ sub p q → sub (pure (_ , p , q)))
+      (λ diamond q∘p → do
+        x , p , q ← q∘p
+        diamond p q)
+```
diff --git a/src/Rewriting/Commute.lagda.md b/src/Rewriting/Commute.lagda.md
new file mode 100644
index 000000000..790c3875e
--- /dev/null
+++ b/src/Rewriting/Commute.lagda.md
@@ -0,0 +1,362 @@
+<!--
+```agda
+open import 1Lab.Prelude
+open import Data.Rel.Base
+open import Data.Rel.Closure
+
+open import Rewriting.Base
+```
+-->
+
+```agda
+module Rewriting.Commute where
+```
+
+<!--
+```agda
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B X : Type ℓ
+  R S _↝₁_ _↝₂_ : Rel A A ℓ
+```
+-->
+
+# Commuting Rewrite Systems
+
+Let $R$ and $S$ be a pair of [abstract rewrite systems] on a
+type $A$. We say that $R$ **commutes** with $S$ if $R^{*}$ and
+$S^{*}$ are resolvable by $S^{*}$ and $R^{*}$, as in the following
+diagram.
+
+[abstract rewrite systems]: Rewriting.Base.html
+
+~~~{.quiver}
+\begin{tikzcd}
+  & x \\
+  y && z \\
+  & {\exists w}
+  \arrow["{S^*}"', dashed, from=2-1, to=3-2]
+  \arrow["{R^*}", dashed, from=2-3, to=3-2]
+  \arrow["{R^*}"', from=1-2, to=2-1]
+  \arrow["{S^*}", from=1-2, to=2-3]
+\end{tikzcd}
+~~~
+
+```agda
+commutes-with : (R : Rel A A ℓ) → (S : Rel A A ℓ') → Type _
+commutes-with R S =
+  is-resolvable
+    (Refl-trans R) (Refl-trans S)
+    (Refl-trans S) (Refl-trans R)
+```
+
+Intuitively, this condition ensures that applying a sequences of rewrites
+from $R$ and $S$ don't let us diverge; we can always reconcile the two
+by performing rewrites from $S$ and $R$, resp. This generalizes
+[confluence], which states that a relation commutes with itself.
+
+[confluence]: Rewriting.Confluence.html
+
+This condition can be somewhat difficult to work with, so we introduce
+an intermediate notion of **semi-commutation**, where one of the reflexive
+transitive closures has been removed.
+
+~~~{.quiver}
+\begin{tikzcd}
+  & x \\
+  y && z \\
+  & {\exists w}
+  \arrow["{S^*}"', dashed, from=2-1, to=3-2]
+  \arrow["{R^*}", dashed, from=2-3, to=3-2]
+  \arrow["{R^*}"', from=1-2, to=2-1]
+  \arrow["S", from=1-2, to=2-3]
+\end{tikzcd}
+~~~
+
+```agda
+semi-commutes-with : (R : Rel A A ℓ) → (S : Rel A A ℓ') → Type _
+semi-commutes-with R S =
+  is-resolvable
+    (Refl-trans R) S
+    (Refl-trans S) (Refl-trans R)
+```
+
+Commutativity obviously implies semi-commutativity.
+
+```agda
+commute→semi-commute : commutes-with R S → semi-commutes-with R S
+commute→semi-commute comm x↝₁*y1 x↝₂y2 =
+  comm x↝₁*y1 [ x↝₂y2 ]
+```
+
+Furthermore, semi-commutativity implies commutativity. We begin with
+the following situation:
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {y_2} \\
+  \\
+  {y_1} && \bullet
+  \arrow["{R^*}"', from=1-1, to=3-1]
+  \arrow["S", from=1-1, to=1-3]
+  \arrow[dashed, from=3-1, to=3-3]
+  \arrow[dashed, from=1-3, to=3-3]
+\end{tikzcd}
+~~~
+
+We then proceed by induction on the $S^*$. If it is an empty sequence of
+rewrites, then we are done. If it is non-empty, then we have the following
+situation:
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {y_2'} && {y_2} \\
+  \\
+  {y_1} &&&& \bullet
+  \arrow["{R^*}"', from=1-1, to=3-1]
+  \arrow["S", from=1-1, to=1-3]
+  \arrow["{S^*}", from=1-3, to=1-5]
+  \arrow[dashed, from=1-5, to=3-5]
+  \arrow[dashed, from=3-1, to=3-5]
+\end{tikzcd}
+~~~
+
+We can apply semi-commutativity to fill in the left-hand square, as
+in the following diagram.
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {y_2'} && {y_2} \\
+  \\
+  {y_1} && {z'} && \bullet
+  \arrow["{R^*}"', from=1-1, to=3-1]
+  \arrow["S", from=1-1, to=1-3]
+  \arrow[dashed, from=1-5, to=3-5]
+  \arrow["{S^*}", from=1-3, to=1-5]
+  \arrow["{S^*}"', from=3-1, to=3-3]
+  \arrow["{R^*}", from=1-3, to=3-3]
+  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=1-1, to=3-3]
+  \arrow[dashed, from=3-3, to=3-5]
+\end{tikzcd}
+~~~
+
+Finally, we can use our induction hypothesis to fill in the right-hand
+square, completing the proof.
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {y_2'} && {y_2} \\
+  \\
+  {y_1} && {z'} && z
+  \arrow["{R^*}"', from=1-1, to=3-1]
+  \arrow["S", from=1-1, to=1-3]
+  \arrow["{R^*}", from=1-5, to=3-5]
+  \arrow["{S^*}", from=1-3, to=1-5]
+  \arrow["{S^*}"', from=3-1, to=3-3]
+  \arrow["{R^*}", from=1-3, to=3-3]
+  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=1-1, to=3-3]
+  \arrow["{S^*}"', from=3-3, to=3-5]
+  \arrow["{I.H.}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=1-3, to=3-5]
+\end{tikzcd}
+~~~
+
+```agda
+semi-commute→commute : semi-commutes-with R S → commutes-with R S
+semi-commute→commute {R = R} {S = S}  semi-comm x↝₁*y1 x↝₂*y2 =
+  Refl-trans-rec-chain
+    (λ x y2 →
+      ∀ y1 → Refl-trans R x y1
+      → is-joinable (Refl-trans S) (Refl-trans R) y1 y2)
+    (λ y1 x↝₁*y1 → pure (y1 , reflexive , x↝₁*y1))
+    (λ {x} {y2'} {y2} x↝₂y2' y2'↝₂*y2 ih y1 x↝₁*y1 → do
+      z' , y1↝₂*z' , y2'↝₁*z' ← semi-comm x↝₁*y1 x↝₂y2'
+      z , z'↝₂*z , y2↝₁*z ← ih z' y2'↝₁*z'
+      pure (z , transitive y1↝₂*z' z'↝₂*z , y2↝₁*z))
+    hlevel!
+    x↝₂*y2 _ x↝₁*y1
+```
+
+## Strong Commutativity
+
+Semi-commutativity is a useful notion when performing purely
+rewrite-theoretic proofs, but it is still difficult to show, as it
+is a global property rather than a local one. For this reason, we
+introduce the notion of **strong commutativity**, which allows us
+to resolve diamonds of the following form:
+
+~~~{.quiver}
+\begin{tikzcd}
+  & x \\
+  y && z \\
+  & {\exists w}
+  \arrow["R"', from=1-2, to=2-1]
+  \arrow["{S^{=}}"', dashed, from=2-1, to=3-2]
+  \arrow["{R^{*}}", dashed, from=2-3, to=3-2]
+  \arrow["S", from=1-2, to=2-3]
+\end{tikzcd}
+~~~
+
+```agda
+strongly-commutes-with : (R : Rel A A ℓ) → (S : Rel A A ℓ') → Type _
+strongly-commutes-with R S =
+  is-resolvable
+    R S
+    (Refl S) (Refl-trans R)
+```
+
+This property is generally easier to show, as it only involves resolving
+one reduction step on either side, instead of an arbitrarily long chain.
+
+As the name suggests, strong commutativity is a stronger condition
+than commutativity. We will prove this by showing that strong
+commutativity implies semi-commutativity.
+
+Recall that semi-commutativity involves resolving a diagram of the
+following shape:
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {y_2} \\
+  \\
+  {y_1} && \bullet
+  \arrow["{R^{*}}"', from=1-1, to=3-1]
+  \arrow["{S^{=}}"', dashed, from=3-1, to=3-3]
+  \arrow["{R^{*}}", dashed, from=1-3, to=3-3]
+  \arrow["S", from=1-1, to=1-3]
+\end{tikzcd}
+~~~
+
+We proceed by induction on the $R^{*}$; if it is an empty path, then
+we are done. If it is non-empty, then we have the following situation:
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {y_2} \\
+  \\
+  {y_1'} \\
+  \\
+  {y_1} && \bullet
+  \arrow["R"', from=1-1, to=3-1]
+  \arrow["{R^{*}}", dashed, from=1-3, to=5-3]
+  \arrow["S", from=1-1, to=1-3]
+  \arrow["{R^{*}}"', from=3-1, to=5-1]
+  \arrow[dashed, from=5-1, to=5-3]
+\end{tikzcd}
+~~~
+
+We can then apply strong commutativity to fill the upper square.
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {y_2} \\
+  \\
+  {y_1'} && {z'} \\
+  \\
+  {y_1} && \bullet
+  \arrow["R"', from=1-1, to=3-1]
+  \arrow["S", from=1-1, to=1-3]
+  \arrow["{R^{*}}"', from=3-1, to=5-1]
+  \arrow["{R{*}}", from=1-3, to=3-3]
+  \arrow["{S^{=}}"', from=3-1, to=3-3]
+  \arrow[dashed, from=3-3, to=5-3]
+  \arrow[dashed, from=5-1, to=5-3]
+  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=1-1, to=3-3]
+\end{tikzcd}
+~~~
+
+We now perform induction on the $S^{=}$. If it is the reflexive path,
+then we have the following situation:
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {y_2} \\
+  \\
+  {y_1'} \\
+  \\
+  {y_1}
+  \arrow["R"', from=1-1, to=3-1]
+  \arrow["S", from=1-1, to=1-3]
+  \arrow["{R^{*}}"', from=3-1, to=5-1]
+  \arrow["{R^{*}}", from=1-3, to=3-1]
+\end{tikzcd}
+~~~
+
+Thus, we can use $y_1$ as our resolution.
+
+If the $S^{=}$ is not the empty path, then we have the following
+diagram:
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {y_2} \\
+  \\
+  {y_1'} && {z'} \\
+  \\
+  {y_1} && \bullet
+  \arrow["R"', from=1-1, to=3-1]
+  \arrow["S", from=1-1, to=1-3]
+  \arrow["{R^{*}}"', from=3-1, to=5-1]
+  \arrow[dashed, from=5-1, to=5-3]
+  \arrow["{R{*}}", from=1-3, to=3-3]
+  \arrow["S"', from=3-1, to=3-3]
+  \arrow[dashed, from=3-3, to=5-3]
+  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=1-1, to=3-3]
+\end{tikzcd}
+~~~
+
+We can use our induction hypothesis to fill in the lower square,
+completing the proof.
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && {y_2} \\
+  \\
+  {y_1'} && {z'} \\
+  \\
+  {y_1} && \bullet
+  \arrow["R"', from=1-1, to=3-1]
+  \arrow["S", from=1-1, to=1-3]
+  \arrow["{R^{*}}"', from=3-1, to=5-1]
+  \arrow["{S^{*}}"', from=5-1, to=5-3]
+  \arrow["{R{*}}", from=1-3, to=3-3]
+  \arrow["S"', from=3-1, to=3-3]
+  \arrow["{R^{*}}", from=3-3, to=5-3]
+  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=1-1, to=3-3]
+  \arrow["{I.H}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=3-1, to=5-3]
+\end{tikzcd}
+~~~
+
+```agda
+strongly-commute→semi-commute
+  : strongly-commutes-with R S → semi-commutes-with R S
+strongly-commute→semi-commute {R = R} {S = S} strong-comm x↝₁*y1 x↝₂y2 =
+  Refl-trans-rec-chain
+    (λ x y1 → ∀ y2 → S x y2 → is-joinable (Refl-trans S) (Refl-trans R) y1 y2)
+    (λ {x} y2 x↝₂y2 → pure (y2 , [ x↝₂y2 ] , reflexive))
+    (λ {x} {y1'} {y1} x↝₁y1' y1'↝₁*y1 ih y2 x↝₂y2 → do
+      z' , y1'↝₂=z , y2↝₁*z ← strong-comm x↝₁y1' x↝₂y2
+      Refl-rec
+       (λ y1' z'
+         → Refl-trans R y2 z' → Refl-trans R y1' y1
+         → (∀ y2 → S y1' y2 → is-joinable (Refl-trans S) (Refl-trans R) y1 y2)
+         → is-joinable (Refl-trans S) (Refl-trans R) y1 y2)
+        (λ {y1'} {z'} y1'↝₂z y2↝₁*z' y1'↝₁*y1 ih → do
+          z , y1↝₂*z , z'↝₁*z ← ih z' y1'↝₂z
+          pure (z , y1↝₂*z , transitive y2↝₁*z' z'↝₁*z))
+       (λ y1' y2↝₁*y1' y1'↝₁*y1 _ →
+         pure (y1 , reflexive , transitive y2↝₁*y1' y1'↝₁*y1))
+       hlevel!
+       y1'↝₂=z y2↝₁*z y1'↝₁*y1 ih)
+    hlevel!
+    x↝₁*y1 _ x↝₂y2
+```
+
+Strong commutativity implies commutativity, as semi-commutativity
+is equivalent to commutativity.
+
+```agda
+strongly-commute→commute
+  : strongly-commutes-with R S → commutes-with R S
+strongly-commute→commute strong-comm =
+  semi-commute→commute $ strongly-commute→semi-commute strong-comm
+```

From 4bd69493aa15e68fa5f330b494d928bb45c0cac4 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Tue, 27 Jun 2023 13:45:25 -0700
Subject: [PATCH 12/19] def: commutative rewrite lemma

---
 .../Rel/Closure/ReflexiveTransitive.lagda.md  |  51 +++-
 src/Rewriting/Base.lagda.md                   |  26 +-
 src/Rewriting/Commute.lagda.md                |  32 +--
 src/Rewriting/Confluent.lagda.md              | 224 ++++++++++++++++--
 4 files changed, 295 insertions(+), 38 deletions(-)

diff --git a/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
index e49aab30c..37207f1ab 100644
--- a/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
+++ b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
@@ -158,7 +158,6 @@ refl-trans-closure .is-rel-closure.closed = refl-trans-clo-closed
 refl-trans-closure .is-rel-closure.has-prop = trunc
 ```
 
-
 ## Properties
 
 If the underlying relation is symmetric, then so is the
@@ -239,3 +238,53 @@ trans-clo-refl-clo≡refl-trans-clo {R = R} =
     trans-clo-refl-clo⊆refl-trans-clo
     refl-trans-clo⊆trans-clo-refl-clo
 ```
+
+The reflexive-transitive closures of $R$ and $S$ are contained in the
+transitive closure of $R \cup S$.
+
+```agda
+refl-trans-clo-inl : Refl-trans R ⊆r Refl-trans (R ∪r S)
+refl-trans-clo-inl =
+  refl-trans-clo-mono (λ r → inc (inl r))
+
+refl-trans-clo-inr : Refl-trans S ⊆r Refl-trans (R ∪r S)
+refl-trans-clo-inr =
+  refl-trans-clo-mono (λ s → inc (inr s))
+```
+
+
+The union of $R$ and $S$ is contained within $S^{*} \circ R^{*}$.
+
+```agda
+union⊆comp-trans-clo
+  : (R ∪r S) ⊆r (Refl-trans S ∘r Refl-trans R)
+union⊆comp-trans-clo {x = x} {y = y} =
+  ∥-∥-map
+    (⊎-rec
+      (λ x↝₁y → y , ([ x↝₁y ] , reflexive))
+      (λ x↝₂y → x , reflexive , [ x↝₂y ]))
+```
+
+The composition of the reflexive-transitive closures of $R$ and $S$ is
+contained within the reflexive-transitive closure of their union.
+
+```agda
+comp-trans-clo⊆trans-clo-union
+  : (Refl-trans S ∘r Refl-trans R) ⊆r Refl-trans (R ∪r S)
+comp-trans-clo⊆trans-clo-union {x = x} {y = y} =
+  ∥-∥-rec trunc
+    (λ { (w , x↝₁w , w↝₂y) →
+      transitive (refl-trans-clo-inl x↝₁w) (refl-trans-clo-inr w↝₂y) })
+```
+
+Therefore, the reflexive-transitive closure of the $R \cup S$
+the reflexive-transitive closure of $S^{*} \circ R^{*}$.
+
+```agda
+refl-trans-clo-union≃refl-trans-clo-comp-refl-trans-clo
+  : Refl-trans (Refl-trans S ∘r Refl-trans R) ≃r Refl-trans (R ∪r S)
+refl-trans-clo-union≃refl-trans-clo-comp-refl-trans-clo =
+  is-rel-closure.⊆+⊆-clo→≃ refl-trans-closure
+    union⊆comp-trans-clo
+    comp-trans-clo⊆trans-clo-union
+```
diff --git a/src/Rewriting/Base.lagda.md b/src/Rewriting/Base.lagda.md
index aa26843b0..dd882ab57 100644
--- a/src/Rewriting/Base.lagda.md
+++ b/src/Rewriting/Base.lagda.md
@@ -15,7 +15,7 @@ module Rewriting.Base where
 private variable
   ℓ ℓ' ℓ'' : Level
   A B X : Type ℓ
-  R S _↝₁_ _↝₂_ : Rel A A ℓ
+  P Q R S P' Q' R' S' : Rel A A ℓ
 ```
 -->
 
@@ -59,6 +59,18 @@ private
   ∘≡joinable = refl
 ```
 
+If $P \subseteq R$ and $Q \subseteq S$, then $R$ and $S$ are joinable
+if $P$ and $Q$ are.
+
+```agda
+joinable-⊆
+  : P ⊆r R → Q ⊆r S
+  → ∀ x y → is-joinable P Q x y → is-joinable R S x y
+joinable-⊆ P⊆R Q⊆S x y = ∥-∥-map λ where
+  (z , p , q) → z , P⊆R p , Q⊆S q
+```
+
+
 Let $P$, $Q$, $R$ and $S$ all be relations on $A$. We say that $P$ and
 $Q$ are resolvable by $R$ and $S$ if for all $x,y,z : A$, $P(x,y)$ and
 $Q(x,z)$ implies that $y$ and $z$ are joinable by $R$ and $S$.
@@ -102,3 +114,15 @@ private
         x , p , q ← q∘p
         diamond p q)
 ```
+
+We also have the following useful lemma characterizing resolvability
+of subrelations.
+
+```agda
+resolvable-⊆
+  : P' ⊆r P → Q' ⊆r Q
+  → R ⊆r R' → S ⊆r S'
+  → is-resolvable P Q R S → is-resolvable P' Q' R' S'
+resolvable-⊆ p q r s sq {x = x} {y = y} x↝y x↝z =
+  joinable-⊆ r s x y (sq (p x↝y) (q x↝z))
+```
diff --git a/src/Rewriting/Commute.lagda.md b/src/Rewriting/Commute.lagda.md
index 790c3875e..db19681cb 100644
--- a/src/Rewriting/Commute.lagda.md
+++ b/src/Rewriting/Commute.lagda.md
@@ -84,8 +84,8 @@ semi-commutes-with R S =
 Commutativity obviously implies semi-commutativity.
 
 ```agda
-commute→semi-commute : commutes-with R S → semi-commutes-with R S
-commute→semi-commute comm x↝₁*y1 x↝₂y2 =
+commutes→semi-commutes : commutes-with R S → semi-commutes-with R S
+commutes→semi-commutes comm x↝₁*y1 x↝₂y2 =
   comm x↝₁*y1 [ x↝₂y2 ]
 ```
 
@@ -135,7 +135,7 @@ in the following diagram.
   \arrow["{S^*}", from=1-3, to=1-5]
   \arrow["{S^*}"', from=3-1, to=3-3]
   \arrow["{R^*}", from=1-3, to=3-3]
-  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=1-1, to=3-3]
+  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=3-3]
   \arrow[dashed, from=3-3, to=3-5]
 \end{tikzcd}
 ~~~
@@ -154,15 +154,15 @@ square, completing the proof.
   \arrow["{S^*}", from=1-3, to=1-5]
   \arrow["{S^*}"', from=3-1, to=3-3]
   \arrow["{R^*}", from=1-3, to=3-3]
-  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=1-1, to=3-3]
+  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=3-3]
   \arrow["{S^*}"', from=3-3, to=3-5]
-  \arrow["{I.H.}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=1-3, to=3-5]
+  \arrow["{I.H.}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-3, to=3-5]
 \end{tikzcd}
 ~~~
 
 ```agda
-semi-commute→commute : semi-commutes-with R S → commutes-with R S
-semi-commute→commute {R = R} {S = S}  semi-comm x↝₁*y1 x↝₂*y2 =
+semi-commutes→commutes : semi-commutes-with R S → commutes-with R S
+semi-commutes→commutes {R = R} {S = S}  semi-comm x↝₁*y1 x↝₂*y2 =
   Refl-trans-rec-chain
     (λ x y2 →
       ∀ y1 → Refl-trans R x y1
@@ -260,7 +260,7 @@ We can then apply strong commutativity to fill the upper square.
   \arrow["{S^{=}}"', from=3-1, to=3-3]
   \arrow[dashed, from=3-3, to=5-3]
   \arrow[dashed, from=5-1, to=5-3]
-  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=1-1, to=3-3]
+  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=3-3]
 \end{tikzcd}
 ~~~
 
@@ -300,7 +300,7 @@ diagram:
   \arrow["{R{*}}", from=1-3, to=3-3]
   \arrow["S"', from=3-1, to=3-3]
   \arrow[dashed, from=3-3, to=5-3]
-  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=1-1, to=3-3]
+  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=3-3]
 \end{tikzcd}
 ~~~
 
@@ -321,15 +321,15 @@ completing the proof.
   \arrow["{R{*}}", from=1-3, to=3-3]
   \arrow["S"', from=3-1, to=3-3]
   \arrow["{R^{*}}", from=3-3, to=5-3]
-  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=1-1, to=3-3]
-  \arrow["{I.H}"{description}, color={rgb,255:red,92;green,92;blue,214}, no body, from=3-1, to=5-3]
+  \arrow["{S.C.}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=3-3]
+  \arrow["{I.H}"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=3-1, to=5-3]
 \end{tikzcd}
 ~~~
 
 ```agda
-strongly-commute→semi-commute
+strongly-commutes→semi-commutes
   : strongly-commutes-with R S → semi-commutes-with R S
-strongly-commute→semi-commute {R = R} {S = S} strong-comm x↝₁*y1 x↝₂y2 =
+strongly-commutes→semi-commutes {R = R} {S = S} strong-comm x↝₁*y1 x↝₂y2 =
   Refl-trans-rec-chain
     (λ x y1 → ∀ y2 → S x y2 → is-joinable (Refl-trans S) (Refl-trans R) y1 y2)
     (λ {x} y2 x↝₂y2 → pure (y2 , [ x↝₂y2 ] , reflexive))
@@ -355,8 +355,8 @@ Strong commutativity implies commutativity, as semi-commutativity
 is equivalent to commutativity.
 
 ```agda
-strongly-commute→commute
+strongly-commutes→commutes
   : strongly-commutes-with R S → commutes-with R S
-strongly-commute→commute strong-comm =
-  semi-commute→commute $ strongly-commute→semi-commute strong-comm
+strongly-commutes→commutes strong-comm =
+  semi-commutes→commutes $ strongly-commutes→semi-commutes strong-comm
 ```
diff --git a/src/Rewriting/Confluent.lagda.md b/src/Rewriting/Confluent.lagda.md
index 8293f8bfe..144066369 100644
--- a/src/Rewriting/Confluent.lagda.md
+++ b/src/Rewriting/Confluent.lagda.md
@@ -4,8 +4,14 @@ open import Rewriting.StronglyNormalising
 
 open import 1Lab.Prelude
 
+open import Data.Rel.Base
 open import Data.Rel.Closure
+open import Data.Sum
 open import Data.Wellfounded.Base
+
+
+open import Rewriting.Base
+open import Rewriting.Commute
 ```
 -->
 
@@ -20,29 +26,19 @@ module Rewriting.Confluent where
 private variable
   ℓ ℓ' ℓ'' : Level
   A B X : Type ℓ
-  R : A → A → Type ℓ
+  R S : A → A → Type ℓ
 ```
 -->
 
-Many problems in computer science can be phrased in terms of
-**term rewriting systems**. Concretely, these are given by a collection
-of terms in some language, along with a collection of rules that describe
-how we can simplify terms. As an example, the untyped $\lambda$-calculus
-can be naturally presented as a term rewriting system, where only
-reduction rule is $\beta$-reduction. More abstractly, a rewriting system
-on a type $A$ is simply a relation $\to$ on $A$ which encodes the
-rewriting rules. Sequences of rewrites are then described using the
-[reflexive transitive closure] of $\to$.
-
-[reflexive transitive closure]: Data.Rel.Closure.html#reflexive-transitive-closure.html
-
-Note that term rewriting systems may be non-deterministic, as multiple
+Recall that [rewriting systems] may be non-deterministic, as multiple
 rewrite rules can apply to a term $t$. This means that multiple
 strategies of applying the rules may lead to different answers, which is
 quite problematic if we want to use the rewriting system to simplify
 expressions. It would be useful if we could prove *some* property of the
 relation that would guarantee that this situation does not occur.
 
+[rewriting systems]: Rewriting.Base.html
+
 This leads us to the notion of **confluence**. We say a relation $\to$
 is confluent if for all pairs of reduction chains $a \to^{*} x$
 and $a \to^{*} y$, there exists some $z$ such that $x \to^{*} z$
@@ -63,8 +59,7 @@ and $y \to^{*} z$, as in the following diagram.
 ```agda
 is-confluent : (A → A → Type ℓ) → Type _
 is-confluent {A = A} R =
-  ∀ {a x y} → Refl-trans R a x → Refl-trans R a y
-  → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z)
+  commutes-with R R
 ```
 
 Note that this does *not* mean that all rewriting sequences terminate
@@ -92,6 +87,23 @@ diverging paths by rewriting to the term at the bottom of the diagram.
 
 <!-- [TODO: Reed M, 02/06/2023] Prove this using Maybe (Nat ^op) -->
 
+Before getting into the more complicated properties of confluence,
+we should get some minor lemmas out of the way. First, if $R^{*}$
+is equivalent to $S^{*}$ and $R^{*}$ is confluent, then so is $S^{*}$.
+This follows directly from properties of resolutions.
+
+```agda
+refl-trans-clo-equiv+confluent→confluent
+  : Refl-trans R ≃r Refl-trans S
+  → is-confluent R → is-confluent S
+refl-trans-clo-equiv+confluent→confluent eqv R-conf {x} {y} {z} =
+  resolvable-⊆
+    (Equiv.from (eqv {x} {y})) (Equiv.from (eqv {x} {z}))
+    (Equiv.to eqv) (Equiv.to eqv)
+    R-conf {x} {y} {z}
+```
+
+
 ## The Church-Rosser Property
 
 A rewriting system $\to$ yields an equivalence relation on terms via
@@ -146,8 +158,8 @@ church-rosser→confluent : has-church-rosser R → is-confluent R
 church-rosser→confluent church-rosser a→*x a→*y =
   church-rosser $
     transitive
-      (symmetric (refl-trans→refl-sym-trans a→*x))
-      (refl-trans→refl-sym-trans a→*y)
+      (symmetric (refl-trans⊆refl-sym-trans a→*x))
+      (refl-trans⊆refl-sym-trans a→*y)
 ```
 
 The converse is much more tricky, and requires introducing an intermediate
@@ -169,8 +181,7 @@ following form.
 ```agda
 is-semi-confluent : (A → A → Type ℓ) → Type _
 is-semi-confluent {A = A} R =
-  ∀ {a x y} → Refl-trans R a x → R a y
-  → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z)
+  semi-commutes-with R R
 ```
 
 Confluence obviously implies semi-confluence.
@@ -515,3 +526,176 @@ strong-normalising+locally-confluent→confluent
         a→*x a→*y ih)
       a a→*x a→*y
 ```
+
+## The Commutative Union Lemma
+
+Confluence proofs can be very fiddly, so it would be useful to be able to
+modularise the proofs somewhat. Ideally, we would be able to split
+a rewriting system $R$ into a union $S \cup T$, and then prove confluence
+of $S$ and $T$ separately. This approach is too naïve, but can be repaired
+by requiring that $S$ and $T$ [commute].
+
+[commute]: Rewriting.Commute.html
+
+The proof of this fact requires some machinery. We say that a rewrite
+system is **strongly confluent** if we can resolve squares of shape (1),
+and that it has the **diamond property** if we can resolve squares of shape
+(2).
+
+~~~{.quiver}
+\begin{tikzcd}
+  & x &&&& x \\
+  y && z && y && z \\
+  & {\exists w} &&&& {\exists w} \\
+  & {(1)} &&&& {(2)}
+  \arrow[from=1-2, to=2-1]
+  \arrow[from=1-2, to=2-3]
+  \arrow[dashed, from=2-5, to=3-6]
+  \arrow[dashed, from=2-7, to=3-6]
+  \arrow[from=1-6, to=2-5]
+  \arrow[from=1-6, to=2-7]
+  \arrow["{*}", dashed, from=2-3, to=3-2]
+  \arrow["{=}"', dashed, from=2-1, to=3-2]
+\end{tikzcd}
+~~~
+
+```agda
+has-diamond : (R : Rel A A ℓ) → Type _
+has-diamond R = is-resolvable R R R R
+
+is-strongly-confluent : (R : Rel A A ℓ) → Type _
+is-strongly-confluent R = strongly-commutes-with R R
+```
+
+The diamond property implies strong confluence, which in turn implies
+confluence.
+
+```agda
+diamond→strongly-confluent : has-diamond R → is-strongly-confluent R
+diamond→strongly-confluent diamond x↝y x↝z = do
+  w , y↝w , x↝w ← diamond x↝y x↝z
+  pure (w , [ y↝w ] , [ x↝w ])
+
+strongly-confluent→confluent : is-strongly-confluent R → is-confluent R
+strongly-confluent→confluent = strongly-commutes→commutes
+
+diamond→confluent : has-diamond R → is-confluent R
+diamond→confluent = strongly-confluent→confluent ∘ diamond→strongly-confluent
+```
+
+With that bit of machinery out of the way, we can proceed with the
+proof.  Recall that if the reflexive-transitive closures of two
+relations are equivalent, then we can transfer confluence across the
+equivalence. Furthermore, the reflexive transitive-closure of $R \cup S$
+is equivalent to the reflexive-transitive closure of $S^{*} \circ
+R^{*}$, so it suffices to show that $S^{*} \circ R^{*}$ is confluent.
+
+We shall do so by establishing that $S^{*} \circ R^{*}$ has the diamond
+property. Doing so requires filling the following diagram:
+
+~~~{.quiver}
+\begin{tikzcd}
+  x & {z'} & z \\
+  {y'} && \bullet \\
+  y & \bullet & \bullet
+  \arrow["{R^{*}}"', from=1-1, to=2-1]
+  \arrow["{S^{*}}"', from=2-1, to=3-1]
+  \arrow["{R^{*}}", from=1-1, to=1-2]
+  \arrow["{S^{*}}", from=1-2, to=1-3]
+  \arrow["{R^{*}}"', dashed, from=3-1, to=3-2]
+  \arrow["{S^{*}}"', dashed, from=3-2, to=3-3]
+  \arrow["{R^{*}}", dashed, from=1-3, to=2-3]
+  \arrow["{S^{*}}", dashed, from=2-3, to=3-3]
+\end{tikzcd}
+~~~
+
+We can use confluence of $R^{*}$ to fill in the upper-left square.
+
+~~~{.quiver}
+\begin{tikzcd}
+  x & {z'} & z \\
+  {y'} & a & \bullet \\
+  y & \bullet & \bullet
+  \arrow["{R^{*}}"', from=1-1, to=2-1]
+  \arrow["{S^{*}}"', from=2-1, to=3-1]
+  \arrow["{R^{*}}", from=1-1, to=1-2]
+  \arrow["{S^{*}}", from=1-2, to=1-3]
+  \arrow["{R^{*}}"', dashed, from=3-1, to=3-2]
+  \arrow["{S^{*}}"', dashed, from=3-2, to=3-3]
+  \arrow["{R^{*}}", dashed, from=1-3, to=2-3]
+  \arrow["{S^{*}}", dashed, from=2-3, to=3-3]
+  \arrow["{R^{*}}"', from=2-1, to=2-2]
+  \arrow["{R^{*}}", from=1-2, to=2-2]
+  \arrow["Conf"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=2-2]
+\end{tikzcd}
+~~~
+
+We can then use commutativity of $R$ and $S$ to fill in the upper-right
+and lower-left squares.
+
+~~~{.quiver}
+\begin{tikzcd}
+  x & {z'} & z \\
+  {y'} & a & c \\
+  y & b & \bullet
+  \arrow["{R^{*}}"', from=1-1, to=2-1]
+  \arrow["{S^{*}}"', from=2-1, to=3-1]
+  \arrow["{R^{*}}", from=1-1, to=1-2]
+  \arrow["{S^{*}}", from=1-2, to=1-3]
+  \arrow["{R^{*}}"', from=3-1, to=3-2]
+  \arrow["{S^{*}}"', dashed, from=3-2, to=3-3]
+  \arrow["{R^{*}}", from=1-3, to=2-3]
+  \arrow["{S^{*}}", dashed, from=2-3, to=3-3]
+  \arrow["{R^{*}}", from=2-1, to=2-2]
+  \arrow["{R^{*}}"', from=1-2, to=2-2]
+  \arrow["{S^{*}}", from=2-2, to=3-2]
+  \arrow["{S^{*}}"', from=2-2, to=2-3]
+  \arrow["Comm"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=2-1, to=3-2]
+  \arrow["Comm"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-2, to=2-3]
+\end{tikzcd}
+~~~
+
+Finally, we can use confluence of $S$ to fill in the lower-right square,
+finishing the proof.
+
+~~~{.quiver}
+\begin{tikzcd}
+  x & {z'} & z \\
+  {y'} & a & c \\
+  y & b & w
+  \arrow["{R^{*}}"', from=1-1, to=2-1]
+  \arrow["{S^{*}}"', from=2-1, to=3-1]
+  \arrow["{R^{*}}", from=1-1, to=1-2]
+  \arrow["{S^{*}}", from=1-2, to=1-3]
+  \arrow["{R^{*}}"', from=3-1, to=3-2]
+  \arrow["{S^{*}}"', from=3-2, to=3-3]
+  \arrow["{R^{*}}", from=1-3, to=2-3]
+  \arrow["{S^{*}}", from=2-3, to=3-3]
+  \arrow["{R^{*}}", from=2-1, to=2-2]
+  \arrow["{R^{*}}"', from=1-2, to=2-2]
+  \arrow["{S^{*}}"', from=2-2, to=3-2]
+  \arrow["{S^{*}}", from=2-2, to=2-3]
+  \arrow["Conf"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=2-2, to=3-3]
+\end{tikzcd}
+~~~
+
+```agda
+commutes+confluent→union-confluent
+  : commutes-with R S
+  → is-confluent R → is-confluent S
+  → is-confluent (R ∪r S)
+commutes+confluent→union-confluent {R = R} {S = S} comm R-conf S-conf =
+  refl-trans-clo-equiv+confluent→confluent
+    refl-trans-clo-union≃refl-trans-clo-comp-refl-trans-clo
+    (diamond→confluent S*∘R*-diamond)
+  where
+    S*∘R*-diamond : has-diamond (Refl-trans S ∘r Refl-trans R)
+    S*∘R*-diamond {x} {y} {z} x↝*y x↝*z = do
+      y' , x↝₁y' , y'↝₂y ← x↝*y
+      z' , x↝₁z' , z'↝₂z ← x↝*z
+      a , y'↝₁a , z'↝₁a ← R-conf x↝₁y' x↝₁z'
+      b , a↝₂b , y↝₁b ← comm y'↝₁a y'↝₂y
+      c , a↝₂c , z↝₁c ← comm z'↝₁a z'↝₂z
+      w , b↝₂w , c↝₂w ← S-conf a↝₂b a↝₂c
+      pure (w , pure (b , y↝₁b , b↝₂w) , pure (c , z↝₁c , c↝₂w))
+```

From 675a98f72b6609cef654c376bdb6db330acb8186 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Tue, 27 Jun 2023 13:45:46 -0700
Subject: [PATCH 13/19] fix: remove redundant import

---
 src/Rewriting/StronglyNormalising.lagda.md | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Rewriting/StronglyNormalising.lagda.md b/src/Rewriting/StronglyNormalising.lagda.md
index ef1c5e327..81354cb28 100644
--- a/src/Rewriting/StronglyNormalising.lagda.md
+++ b/src/Rewriting/StronglyNormalising.lagda.md
@@ -1,7 +1,6 @@
 <!--
 ```agda
 open import 1Lab.Prelude
-open import Data.Dec
 open import Data.Rel.Closure
 open import Data.Wellfounded.Base
 ```

From eafa9ebea771b0c1c3d6e7a64545ca3e6e8bb257 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Wed, 28 Jun 2023 11:09:29 -0700
Subject: [PATCH 14/19] =?UTF-8?q?refactor:=20rename=20=E2=88=A5-=E2=88=A5-?=
 =?UTF-8?q?proj=20to=20=E2=88=A5-=E2=88=A5-proj!?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/1Lab/HIT/Truncation.lagda.md          |  7 +++++--
 src/Cat/Univalent/Rezk/Universal.lagda.md | 22 +++++++++++-----------
 src/Data/Fin/Finite.lagda.md              | 10 +++++-----
 src/Data/Set/Material.lagda.md            |  6 +++---
 src/Order/Semilattice/Free.lagda.md       |  6 +++---
 5 files changed, 27 insertions(+), 24 deletions(-)

diff --git a/src/1Lab/HIT/Truncation.lagda.md b/src/1Lab/HIT/Truncation.lagda.md
index 51ee73809..b9c30b999 100644
--- a/src/1Lab/HIT/Truncation.lagda.md
+++ b/src/1Lab/HIT/Truncation.lagda.md
@@ -106,8 +106,11 @@ whenever it is a family of propositions, by providing a case for
   → (x : ∥ A ∥) → P
 ∥-∥-rec! {pprop = pprop} = ∥-∥-elim (λ _ → pprop)
 
-∥-∥-proj : ∀ {ℓ} {A : Type ℓ} → {@(tactic hlevel-tactic-worker) ap : is-prop A} → ∥ A ∥ → A
-∥-∥-proj {ap = ap} = ∥-∥-rec ap λ x → x
+∥-∥-proj : ∀ {ℓ} {A : Type ℓ} → is-prop A → ∥ A ∥ → A
+∥-∥-proj ap = ∥-∥-rec ap λ x → x
+
+∥-∥-proj! : ∀ {ℓ} {A : Type ℓ} → {@(tactic hlevel-tactic-worker) ap : is-prop A} → ∥ A ∥ → A
+∥-∥-proj! {ap = ap} = ∥-∥-proj ap
 ```
 -->
 
diff --git a/src/Cat/Univalent/Rezk/Universal.lagda.md b/src/Cat/Univalent/Rezk/Universal.lagda.md
index d11f23185..b5598e396 100644
--- a/src/Cat/Univalent/Rezk/Universal.lagda.md
+++ b/src/Cat/Univalent/Rezk/Universal.lagda.md
@@ -86,7 +86,7 @@ eso→pre-faithful
   → is-eso H → (γ δ : F => G)
   → (∀ b → γ .η (H .F₀ b) ≡ δ .η (H .F₀ b)) → γ ≡ δ
 eso→pre-faithful {A = A} {B = B} {C = C} H {F} {G} h-eso γ δ p =
-  Nat-path λ b → ∥-∥-proj {ap = C.Hom-set _ _ _ _} do
+  Nat-path λ b → ∥-∥-proj (C.Hom-set _ _ _ _) do
   (b′ , m) ← h-eso b
   ∥_∥.inc $
     γ .η b                                      ≡⟨ C.intror (F-map-iso F m .invl) ⟩
@@ -191,7 +191,7 @@ this file in Agda and poke around the proof.
 ```agda
       lemma : (a : A.Ob) (f : H.₀ a B.≅ b)
             → γ.η a ≡ G.₁ (f .from) C.∘ g C.∘ F.₁ (f .to)
-      lemma a f = ∥-∥-proj {ap = C.Hom-set _ _ _ _} do
+      lemma a f = ∥-∥-proj (C.Hom-set _ _ _ _) do
         (k , p)   ← H-full (h.from B.∘ B.to f)
         (k⁻¹ , q) ← H-full (B.from f B.∘ h.to)
         ∥_∥.inc $
@@ -216,7 +216,7 @@ over $b$ is a proposition.
     T-prop : ∀ b → is-prop (T b)
     T-prop b (g , coh) (g′ , coh′) =
       Σ-prop-path (λ x → Π-is-hlevel² 1 λ _ _ → C.Hom-set _ _ _ _) $
-        ∥-∥-proj {ap = C.Hom-set _ _ _ _} do
+        ∥-∥-proj (C.Hom-set _ _ _ _) do
         (a₀ , h) ← H-eso b
         pure $ C.iso→epic (F-map-iso F h) _ _
           (C.iso→monic (F-map-iso G (h B.Iso⁻¹)) _ _
@@ -236,7 +236,7 @@ $(a,h)$ pair.
       ∥_∥.inc (Mk.g b a₀ h , Mk.lemma b a₀ h)
 
     mkT : ∀ b → T b
-    mkT b = ∥-∥-proj {ap = T-prop b} (mkT′ b (H-eso b))
+    mkT b = ∥-∥-proj (T-prop b) (mkT′ b (H-eso b))
 ```
 
 Another calculation shows that, since $H$ is full, given any pair of
@@ -260,7 +260,7 @@ the transformation we're defining, too.
         module h = B._≅_ h
 
       naturality : _
-      naturality = ∥-∥-proj {ap = C.Hom-set _ _ _ _} do
+      naturality = ∥-∥-proj (C.Hom-set _ _ _ _) do
         (k , p) ← H-full (h′.from B.∘ f B.∘ h.to)
         pure $ C.pullr (C.pullr (F.weave (sym
                   (B.pushl p ∙ ap₂ B._∘_ refl (B.cancelr h.invl)))))
@@ -281,8 +281,8 @@ $- \circ H$ is faithful, and now we've shown it is full, it is fully faithful.
     δ : F => G
     δ .η b = mkT b .fst
     δ .is-natural b b′ f = ∥-∥-elim₂
-      {P = λ α β → ∥-∥-proj {ap = T-prop b′} (mkT′ b′ α) .fst C.∘ F.₁ f
-                 ≡ G.₁ f C.∘ ∥-∥-proj {ap = T-prop b} (mkT′ b β) .fst}
+      {P = λ α β → ∥-∥-proj (T-prop b′) (mkT′ b′ α) .fst C.∘ F.₁ f
+                 ≡ G.₁ f C.∘ ∥-∥-proj (T-prop b) (mkT′ b β) .fst}
       (λ _ _ → C.Hom-set _ _ _ _)
       (λ (a′ , h′) (a , h) → naturality f a a′ h h′) (H-eso b′) (H-eso b)
 
@@ -290,7 +290,7 @@ $- \circ H$ is faithful, and now we've shown it is full, it is fully faithful.
   full {x = x} {y = y} γ = pure (δ _ _ γ , Nat-path p) where
     p : ∀ b → δ _ _ γ .η (H.₀ b) ≡ γ .η b
     p b = subst
-      (λ e → ∥-∥-proj {ap = T-prop _ _ γ (H.₀ b)} (mkT′ _ _ γ (H.₀ b) e) .fst
+      (λ e → ∥-∥-proj (T-prop _ _ γ (H.₀ b)) (mkT′ _ _ γ (H.₀ b) e) .fst
            ≡ γ .η b)
       (squash (inc (b , B.id-iso)) (H-eso (H.₀ b)))
       (C.eliml (y .F-id) ∙ C.elimr (x .F-id))
@@ -377,7 +377,7 @@ candidate over it.
 <!--
 ```agda
     summon : ∀ {b} → ∥ Essential-fibre H b ∥ → is-contr (Obs b)
-    summon f = ∥-∥-proj {ap = is-contr-is-prop} do
+    summon f = ∥-∥-proj is-contr-is-prop do
       f ← f
       pure $ contr (obj′ f) (Obs-is-prop f)
 
@@ -488,7 +488,7 @@ This proof _really_ isn't commented. I'm sorry.
         (λ _ → compat-prop f) (sym (Homs-prop′ f _ _ _ _ h′)))
 
     Homs-contr : ∀ {b b′} (f : B.Hom b b′) → is-contr (Homs f)
-    Homs-contr f = ∥-∥-proj (Homs-contr′ f)
+    Homs-contr f = ∥-∥-proj! (Homs-contr′ f)
 
     G₁ : ∀ {b b′} → B.Hom b b′ → C.Hom (G₀ b) (G₀ b′)
     G₁ f = Homs-contr f .centre .fst
@@ -552,7 +552,7 @@ a set --- a proposition --- these choices don't matter, so we can use
 essential surjectivity of $H$.
 
 ```agda
-    G .F-∘ {x} {y} {z} f g = ∥-∥-proj do
+    G .F-∘ {x} {y} {z} f g = ∥-∥-proj! do
       (ax , hx) ← H-eso x
       (ay , hy) ← H-eso y
       (az , hz) ← H-eso z
diff --git a/src/Data/Fin/Finite.lagda.md b/src/Data/Fin/Finite.lagda.md
index 510987489..1c949d104 100644
--- a/src/Data/Fin/Finite.lagda.md
+++ b/src/Data/Fin/Finite.lagda.md
@@ -93,11 +93,11 @@ open Finite ⦃ ... ⦄ public
 instance
   H-Level-Finite : ∀ {ℓ} {A : Type ℓ} {n : Nat} → H-Level (Finite A) (suc n)
   H-Level-Finite = prop-instance {T = Finite _} λ where
-    x y i .Finite.cardinality → ∥-∥-proj
+    x y i .Finite.cardinality → ∥-∥-proj!
       ⦇ Fin-injective (⦇ ⦇ x .enumeration e⁻¹ ⦈ ∙e y .enumeration ⦈) ⦈
       i
     x y i .Finite.enumeration → is-prop→pathp
-      {B = λ i → ∥ _ ≃ Fin (∥-∥-proj ⦇ Fin-injective (⦇ ⦇ x .enumeration e⁻¹ ⦈ ∙e y .enumeration ⦈) ⦈ i) ∥}
+      {B = λ i → ∥ _ ≃ Fin (∥-∥-proj! ⦇ Fin-injective (⦇ ⦇ x .enumeration e⁻¹ ⦈ ∙e y .enumeration ⦈) ⦈ i) ∥}
       (λ _ → squash)
       (x .enumeration) (y .enumeration) i
 
@@ -146,7 +146,7 @@ private
     .snd .is-iso.rinv fzero → refl
     .snd .is-iso.linv x → funext λ { () }
 
-  finite-pi-fin (suc sz) {B} fam = ∥-∥-proj $ do
+  finite-pi-fin (suc sz) {B} fam = ∥-∥-proj! $ do
     e ← finite-choice (suc sz) λ x → fam x .enumeration
     let rest = finite-pi-fin sz (λ x → fam (fsuc x))
     cont ← rest .Finite.enumeration
@@ -167,13 +167,13 @@ Finite-⊎ {A = A} {B = B} = fin $ do
   beq ← enumeration {T = B}
   pure (⊎-ap aeq beq ∙e Finite-coproduct)
 
-Finite-Π {A = A} {P = P} ⦃ fin {sz} en ⦄ ⦃ fam ⦄ = ∥-∥-proj $ do
+Finite-Π {A = A} {P = P} ⦃ fin {sz} en ⦄ ⦃ fam ⦄ = ∥-∥-proj! $ do
   eqv ← en
   let count = finite-pi-fin sz λ x → fam $ equiv→inverse (eqv .snd) x
   eqv′ ← count .Finite.enumeration
   pure $ fin $ pure $ Π-dom≃ (eqv e⁻¹) ∙e eqv′
 
-Finite-Σ {A = A} {P = P} ⦃ afin ⦄ ⦃ fam ⦄ = ∥-∥-proj $ do
+Finite-Σ {A = A} {P = P} ⦃ afin ⦄ ⦃ fam ⦄ = ∥-∥-proj! $ do
   aeq ← afin .Finite.enumeration
   let
     module aeq = Equiv aeq
diff --git a/src/Data/Set/Material.lagda.md b/src/Data/Set/Material.lagda.md
index e8fbae44f..9d192662c 100644
--- a/src/Data/Set/Material.lagda.md
+++ b/src/Data/Set/Material.lagda.md
@@ -285,8 +285,8 @@ Presentation-is-prop {ℓ} {A} f P1 P2 = done where
 
   eqv : ∀ x → fibre g x ≃ fibre h x
   eqv x = prop-ext (gm x) (hm x)
-    (λ fib → ∥-∥-proj {ap = hm x} (v' .fst x (u' .snd x (inc fib))))
-    (λ fib → ∥-∥-proj {ap = gm x} (u' .fst x (v' .snd x (inc fib))))
+    (λ fib → ∥-∥-proj (hm x) (v' .fst x (u' .snd x (inc fib))))
+    (λ fib → ∥-∥-proj (gm x) (u' .fst x (v' .snd x (inc fib))))
 ```
 
 This pointwise equivalence between fibres extends to an equivalence
@@ -386,7 +386,7 @@ module Members {ℓ} (X : V ℓ) where
 
   memb : ∀ {x} → x ∈ₛ X ≃ fibre elem x
   memb {x = x} = prop-ext (is-member _ X .is-tr) (embeds _)
-    (λ a → ∥-∥-proj {ap = embeds _} (subst (x ∈ₛ_) presents a))
+    (λ a → ∥-∥-proj (embeds _) (subst (x ∈ₛ_) presents a))
     (λ a → subst (x ∈ₛ_) (sym presents) (inc a))
 
   module memb {x} = Equiv (memb {x})
diff --git a/src/Order/Semilattice/Free.lagda.md b/src/Order/Semilattice/Free.lagda.md
index 688d38e46..66fd54ef8 100644
--- a/src/Order/Semilattice/Free.lagda.md
+++ b/src/Order/Semilattice/Free.lagda.md
@@ -194,7 +194,7 @@ $K$-finiteness condition, but it will be very useful!
       .glb≤fam i →
         K-fin-lt {P , P-fin} {ηₛₗ (cover i .fst)} λ j i=j →
           subst (λ e → ∣ P e ∣) (out! i=j) (cover i .snd)
-      .greatest lb′ wit → K-fin-lt {lb′} {P , P-fin} λ i i∈p → ∥-∥-proj do
+      .greatest lb′ wit → K-fin-lt {lb′} {P , P-fin} λ i i∈p → ∥-∥-proj! do
         (idx , path) ← surj (i , i∈p)
         pure (K-fin-lt′ {lb′} {ηₛₗ (cover idx .fst)} (wit idx) i (inc (ap fst path)))
 ```
@@ -267,7 +267,7 @@ make-free-slat .universal {x} {y} f = total-hom go pres where
   pres .pres-⋆ (A , af) (B , bf) =
     ap fst $
       glb-unique y.po (go.ε′ (_∪_ x (A , af) (B , bf) .fst) (_∪_ x (A , af) (B , bf) .snd)) $ _ , λ where
-        .glb≤fam (x , w) → ∥-∥-proj $ w >>= λ where
+        .glb≤fam (x , w) → ∥-∥-proj! $ w >>= λ where
           (inl w) → pure $
             g1 .fst y.∩ g2 .fst y.≤⟨ y.∩≤l ⟩
             g1 .fst             y.≤⟨ g1.glb≤fam (x , w) ⟩
@@ -287,7 +287,7 @@ make-free-slat .universal {x} {y} f = total-hom go pres where
 make-free-slat .commutes {y = y} f = funext λ x → sym y.∩-idr
   where module y = Semilattice y
 make-free-slat .unique {x = x} {y = y} {f = f} {g = g} w =
-  Homomorphism-path λ arg → ∥-∥-proj {ap = y.has-is-set _ _} do
+  Homomorphism-path λ arg → ∥-∥-proj (y.has-is-set _ _) do
     (card , diagram , glb) ← K-reduce x arg
     let
       path : arg ≡ KA.⋂ λ i → ηₛₗ x (diagram i)

From aa6aeb440ee83b92348b170b7a7312e0e85a7a95 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Wed, 28 Jun 2023 11:39:16 -0700
Subject: [PATCH 15/19] def: normal forms, confluence implies uniqueness

---
 .../Rel/Closure/ReflexiveTransitive.lagda.md  | 23 ++++++
 src/Rewriting/Base.lagda.md                   | 73 +++++++++++++++++++
 src/Rewriting/Confluent.lagda.md              | 23 ++++++
 src/Rewriting/StronglyNormalising.lagda.md    |  2 +-
 4 files changed, 120 insertions(+), 1 deletion(-)

diff --git a/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
index 37207f1ab..fc59f59c7 100644
--- a/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
+++ b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
@@ -132,6 +132,29 @@ Refl-trans-case-fork {R' = R'} {R = R} S refll reflr fork prop {a} {x} {y} a→*
     a→*x a→*y
 ```
 
+Similarly, we provide an eliminator for inspecting wedges.
+
+```agda
+Refl-trans-case-wedge
+  : (S : A → A → A → Type ℓ)
+  → (∀ {z} → S z z z)
+  → (∀ {x y y' z} → R' y y' → Refl-trans R' y' z → S x y z)
+  → (∀ {x x' y z} → R x x' → Refl-trans R x' z → S x y z)
+  → (∀ {x y z} → is-prop (S x y z))
+  → ∀ {x y z} → Refl-trans R x z → Refl-trans R' y z → S x y z
+Refl-trans-case-wedge {R' = R'} {R = R} S refl2 wedgel wedger prop {x} {y} {z} x→*z y→*z =
+  Refl-trans-rec-chain (λ x z → Refl-trans R' y z → S x y z)
+    (λ y→*z → Refl-trans-rec-chain (λ y z → S z y z)
+      refl2
+      (λ y→y' y'→*z _ → wedgel y→y' y'→*z)
+      prop
+      y→*z)
+    (λ x→x' x'→z _ _ → wedger x→x' x'→z)
+    (Π-is-hlevel 1 λ _ → prop)
+    x→*z y→*z
+```
+
+
 ## As a closure operator
 
 ```agda
diff --git a/src/Rewriting/Base.lagda.md b/src/Rewriting/Base.lagda.md
index dd882ab57..989cd1ad7 100644
--- a/src/Rewriting/Base.lagda.md
+++ b/src/Rewriting/Base.lagda.md
@@ -126,3 +126,76 @@ resolvable-⊆
 resolvable-⊆ p q r s sq {x = x} {y = y} x↝y x↝z =
   joinable-⊆ r s x y (sq (p x↝y) (q x↝z))
 ```
+
+## Normal Forms
+
+Let $R$ be an abstract rewriting relation on a type $A$. We say
+that an element $x : A$ is a **normal form** if it cannot be reduced
+by $R$.
+
+```agda
+is-normal-form : (R : Rel A A ℓ) → A → Type _
+is-normal-form {A = A} R x = ¬ Σ[ y ∈ A ] R x y
+```
+
+A normal form of $x : A$ is another $y : A$ such that $y$ is a normal form
+and $R^{*}(x,y)$. Note that this is untruncated; uniqueness of normal forms
+shall be derived from other properties of $R$.
+
+```agda
+record Normal-form {A : Type ℓ} (R : Rel A A ℓ') (x : A) : Type (ℓ ⊔ ℓ') where
+  constructor normal-form
+  no-eta-equality
+  field
+    nf : A
+    reduces : Refl-trans R x nf
+    has-normal-form : is-normal-form R nf
+
+open Normal-form
+```
+
+If $A$ is a set, then the type of normal forms is also a set.
+
+```agda
+private unquoteDecl eqv = declare-record-iso eqv (quote Normal-form)
+
+Normal-form-is-hlevel
+  : ∀ {R : A → A → Type ℓ} {x}
+  → (n : Nat) → is-hlevel A (2 + n) → is-hlevel (Normal-form R x) (2 + n)
+Normal-form-is-hlevel n A-set =
+  Iso→is-hlevel (2 + n) eqv (Σ-is-hlevel (2 + n) A-set hlevel!)
+```
+
+<!--
+```agda
+instance
+  H-Level-normal-form
+    : ∀ {R : A → A → Type ℓ} {x} {n}
+    → ⦃ A-hlevel : ∀ {n} → H-Level A (2 + n) ⦄ → H-Level (Normal-form R x) (2 + n)
+  H-Level-normal-form ⦃ A-hlevel ⦄ =
+    basic-instance 2 (Normal-form-is-hlevel 0 (H-Level.has-hlevel {n = 2} A-hlevel))
+
+Normal-form-pathp
+  : ∀ {x y}
+  → (p : x ≡ y)
+  → (x-nf : Normal-form R x) → (y-nf : Normal-form R y)
+  → x-nf .nf ≡ y-nf. nf
+  → PathP (λ i → Normal-form R (p i)) x-nf y-nf
+Normal-form-pathp p x-nf y-nf nf-path i .nf = nf-path i
+Normal-form-pathp {R = R} p x-nf y-nf nf-path i .reduces =
+  is-prop→pathp {B = λ i → Refl-trans R (p i) (nf-path i)}
+    (λ i → trunc)
+    (x-nf .reduces) (y-nf .reduces) i
+Normal-form-pathp {R = R} p x-nf y-nf nf-path i .has-normal-form =
+  is-prop→pathp {B = λ i → is-normal-form R (nf-path i)}
+    (λ i → hlevel!)
+    (x-nf .has-normal-form) (y-nf .has-normal-form) i
+
+Normal-form-path
+  : ∀ {x}
+  → (x-nf x-nf' : Normal-form R x)
+  → x-nf .nf ≡ x-nf'. nf
+  → x-nf ≡ x-nf'
+Normal-form-path x-nf x-nf' p = Normal-form-pathp refl x-nf x-nf' p
+```
+-->
diff --git a/src/Rewriting/Confluent.lagda.md b/src/Rewriting/Confluent.lagda.md
index 144066369..ee3233ab2 100644
--- a/src/Rewriting/Confluent.lagda.md
+++ b/src/Rewriting/Confluent.lagda.md
@@ -103,6 +103,29 @@ refl-trans-clo-equiv+confluent→confluent eqv R-conf {x} {y} {z} =
     R-conf {x} {y} {z}
 ```
 
+If a rewrite system on a set is confluent, then every element of $A$
+has at most one normal form.
+
+```agda
+confluent→unique-normal-forms
+  : ∀ {R : A → A → Type ℓ}
+  → is-set A
+  → is-confluent R 
+  → ∀ x → is-prop (Normal-form R x)
+confluent→unique-normal-forms {R = R} A-set conf x y-nf z-nf =
+  ∥-∥-proj (Normal-form-is-hlevel 0 A-set y-nf z-nf) $ do
+    w , y↝w , z↝w ← conf (y-nf .reduces) (z-nf .reduces)
+    p ← Refl-trans-case-wedge
+         (λ y z w → is-normal-form R y → is-normal-form R z → ∥ y ≡ z ∥)
+         (λ _ _ → inc refl)
+         (λ z→z' _ _ z-nf → absurd (z-nf (_ , z→z')))
+         (λ y→y' _ y-nf _ → absurd (y-nf (_ , y→y')))
+         hlevel!
+         y↝w z↝w (y-nf .has-normal-form) (z-nf .has-normal-form)
+    pure (Normal-form-path y-nf z-nf p)
+    where open Normal-form
+```
+
 
 ## The Church-Rosser Property
 
diff --git a/src/Rewriting/StronglyNormalising.lagda.md b/src/Rewriting/StronglyNormalising.lagda.md
index 81354cb28..02f281549 100644
--- a/src/Rewriting/StronglyNormalising.lagda.md
+++ b/src/Rewriting/StronglyNormalising.lagda.md
@@ -56,7 +56,7 @@ step $a_0 \leadsto a_1$ of the sequence.
 ```agda
 strongly-normalising→terminating : is-strongly-normalising _↝_ → is-terminating _↝_
 strongly-normalising→terminating {_↝_ = _↝_} sn ∥chain∥ =
-  ∥-∥-proj $ do
+  ∥-∥-proj! $ do
     (aₙ , step) ← ∥chain∥
     inc $ Wf-induction _ sn
       (λ a → ∀ n → ¬ Trans _↝_ a (aₙ (suc n)))

From b122f6bb9e4ab4a26dfef9b516022830feec9b90 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Wed, 28 Jun 2023 13:45:20 -0700
Subject: [PATCH 16/19] def: more lemmas about normal forms

---
 .../Rel/Closure/ReflexiveTransitive.lagda.md  |  21 +++
 src/Rewriting/Base.lagda.md                   |  52 ++++++
 src/Rewriting/Confluent.lagda.md              | 155 +++++++++++++++++-
 3 files changed, 226 insertions(+), 2 deletions(-)

diff --git a/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
index fc59f59c7..468c4f179 100644
--- a/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
+++ b/src/Data/Rel/Closure/ReflexiveTransitive.lagda.md
@@ -1,6 +1,7 @@
 <!--
 ```agda
 open import 1Lab.Prelude
+open import Data.Maybe.Base
 open import Data.Sum
 
 open import Data.Rel.Base
@@ -105,6 +106,26 @@ Refl-trans-rec-chain {R = R} S pnil pstep pprop r+ = go r+ reflexive pnil where
     pprop (go x→*y y→*z acc) (go x→*y' y→*z acc) i
 ```
 
+It's useful to be able to perform induction in the reverse direction, so
+we also provide a recursion principle for doing so.
+
+```agda
+Refl-trans-rec-chain-bwd
+  : (S : A → A → Type ℓ)
+  → (∀ {x} → S x x)
+  → (∀ {x y z} → Refl-trans R x y → R y z → S x y → S x z)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → Refl-trans R x y → S x y
+Refl-trans-rec-chain-bwd {R = R} S pnil pstep pprop {x = x} r+ =
+  Refl-trans-rec-chain (λ y z → Refl-trans R x y → S x y → S x z)
+    (λ _ Sxx' → Sxx')
+    (λ {x'} {y} {z} x'→y y→*z ih x→*x' Sxx' →
+      ih (transitive x→*x' [ x'→y ]) (pstep x→*x' x'→y Sxx'))
+    (Π-is-hlevel 1 λ _ → Π-is-hlevel 1 λ _ → pprop)
+    r+ reflexive pnil
+```
+
+
 We also provide an eliminator for inspecting forks.
 
 ```agda
diff --git a/src/Rewriting/Base.lagda.md b/src/Rewriting/Base.lagda.md
index 989cd1ad7..bee74e411 100644
--- a/src/Rewriting/Base.lagda.md
+++ b/src/Rewriting/Base.lagda.md
@@ -138,6 +138,58 @@ is-normal-form : (R : Rel A A ℓ) → A → Type _
 is-normal-form {A = A} R x = ¬ Σ[ y ∈ A ] R x y
 ```
 
+This allows us to give a restricted form of elimination for the
+reflexive-transitive closure when the domain is a normal form.
+
+```agda
+Refl-trans-rec-normal-form
+  : (S : A → A → Type ℓ)
+  → (∀ {x} → S x x)
+  → (∀ {x y} → is-prop (S x y))
+  → ∀ {x y} → is-normal-form R x → Refl-trans R x y → S x y
+Refl-trans-rec-normal-form {R = R} S srefl sprop x-nf x↝y =
+  Refl-trans-rec-chain
+    (λ x y → is-normal-form R x → S x y)
+    (λ _ → srefl)
+    (λ x↝y _ _ x-nf → absurd (x-nf (_ , x↝y)))
+    (Π-is-hlevel 1 λ _ → sprop)
+    x↝y x-nf
+```
+
+
+If if $A$ is a set, $x : A$ is a normal form, and $x \to^{*} y$, then
+$x = y$.
+
+```agda
+normal-form+reduces→path
+  : ∀ {R : Rel A A ℓ} {x y}
+  → is-set A
+  → is-normal-form R x
+  → Refl-trans R x y
+  → x ≡ y
+normal-form+reduces→path {R = R} A-set =
+  Refl-trans-rec-normal-form _≡_ refl (A-set _ _)
+```
+
+<!-- [TODO: Reed M, 28/06/2023] Prove that this yields a pointed identity system -->
+
+If $x$ is a normal form, and $x \to^{*} z$ and $y \to^{*} z$, then
+$y$ must reduce to $x$.
+
+```agda
+normal-form+reduces→reduces
+  : ∀ {R : Rel A A ℓ} {x y z}
+  → is-normal-form R x
+  → Refl-trans R x z → Refl-trans R y z
+  → Refl-trans R y x
+normal-form+reduces→reduces {R = R} {y = y} x-nf x↝z y↝z =
+  Refl-trans-rec-normal-form
+    (λ x z → Refl-trans R y z → Refl-trans R y x)
+    id
+    hlevel!
+    x-nf x↝z y↝z
+```
+
 A normal form of $x : A$ is another $y : A$ such that $y$ is a normal form
 and $R^{*}(x,y)$. Note that this is untruncated; uniqueness of normal forms
 shall be derived from other properties of $R$.
diff --git a/src/Rewriting/Confluent.lagda.md b/src/Rewriting/Confluent.lagda.md
index ee3233ab2..7210a3fec 100644
--- a/src/Rewriting/Confluent.lagda.md
+++ b/src/Rewriting/Confluent.lagda.md
@@ -27,6 +27,8 @@ private variable
   ℓ ℓ' ℓ'' : Level
   A B X : Type ℓ
   R S : A → A → Type ℓ
+
+open Normal-form
 ```
 -->
 
@@ -108,7 +110,7 @@ has at most one normal form.
 
 ```agda
 confluent→unique-normal-forms
-  : ∀ {R : A → A → Type ℓ}
+  : ∀ {R : Rel A A ℓ}
   → is-set A
   → is-confluent R 
   → ∀ x → is-prop (Normal-form R x)
@@ -123,9 +125,76 @@ confluent→unique-normal-forms {R = R} A-set conf x y-nf z-nf =
          hlevel!
          y↝w z↝w (y-nf .has-normal-form) (z-nf .has-normal-form)
     pure (Normal-form-path y-nf z-nf p)
-    where open Normal-form
 ```
 
+<!--
+```agda
+-- Useful for local instances.
+H-Level-confluent-normal-form
+  : ∀ {R : Rel A A ℓ} {x} {n}
+  → is-set A
+  → is-confluent R
+  → H-Level (Normal-form R x) (suc n)
+H-Level-confluent-normal-form set conf =
+  prop-instance (confluent→unique-normal-forms set conf _)
+```
+-->
+
+If $\to$ is a confluent relation and $x \to^{*} w \leftarrow^{*} y$,
+then $y$ has a normal form if and only if $x$ does.
+
+To see this, note that we have the following pair of reductions
+out of $x$:
+
+~~~{.quiver}
+\begin{tikzcd}
+        x && w && y \\
+        \\
+        {x \downarrow}
+        \arrow["{*}", from=1-1, to=1-3]
+        \arrow["{*}"', from=1-1, to=3-1]
+        \arrow["{*}"', from=1-5, to=1-3]
+\end{tikzcd}
+~~~
+
+We can use confluence to fill in the left-hand square:
+
+~~~{.quiver}
+\begin{tikzcd}
+  x && w && y \\
+  \\
+  {x \downarrow} && {w'}
+  \arrow["{*}", from=1-1, to=1-3]
+  \arrow["{*}"', from=1-1, to=3-1]
+  \arrow["{*}"', from=1-5, to=1-3]
+  \arrow[from=1-3, to=3-3]
+  \arrow[from=3-1, to=3-3]
+  \arrow["Conf"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-1, to=3-3]
+\end{tikzcd}
+~~~
+
+Note that $x \downarrow$ and $y$ both reduce to the same value; this
+means that $y$ reduces to $x \downarrow$, as $x \downarrow$ is a normal
+form.
+
+```agda
+confluent+wedge+normal-form→normal-form
+  : ∀ {x y w}
+  → is-confluent R
+  → Refl-trans R x w → Refl-trans R y w
+  → Normal-form R x → Normal-form R y
+confluent+wedge+normal-form→normal-form conf x↝w y↝w x↓ .nf =
+  x↓ .nf
+confluent+wedge+normal-form→normal-form conf x↝w y↝w x↓ .reduces =
+  ∥-∥-rec!
+    (λ where
+      (w' , x↓↝w' , w↝w') →
+        normal-form+reduces→reduces (x↓ .has-normal-form)
+          x↓↝w' (transitive y↝w w↝w'))
+    (conf (x↓ .reduces) x↝w)
+confluent+wedge+normal-form→normal-form conf x↝w y↝w x↓ .has-normal-form =
+  x↓ .has-normal-form
+```
 
 ## The Church-Rosser Property
 
@@ -379,6 +448,88 @@ church-rosser→semiconfluent church-rosser =
   confluent→semiconfluent (church-rosser→confluent church-rosser)
 ```
 
+This theorem has some very useful consequences; first, if $R$ is
+confluent and $x$ and $y$ are convertible, then $x$ reduces to $y$
+if $y$ is in normal form.
+
+To see this, note that Church-rosser implies that gives us a $w$ such
+that $x \to^{*} w$ and $y \to^{*} w$. We can then perform induction
+on the $y \to^{*} w$; if it is empty, then we have $y = w$, and thus
+$x \to^{*} y$. If it is non-empty, then we have a contradiction, as
+$y$ is a normal form.
+
+```agda
+confluent+convertible→reduces-to-normal-form
+  : ∀ {x y}
+  → is-confluent R
+  → Refl-sym-trans R x y
+  → is-normal-form R y
+  → Refl-trans R x y
+confluent+convertible→reduces-to-normal-form {R = R} {x = x} {y = y} conf x↔y y-nf =
+  ∥-∥-rec!
+    (λ where
+      (w , x↝w , y↝w) →
+        Refl-trans-rec-chain
+          (λ y w → is-normal-form R y → Refl-trans R x w → Refl-trans R x y)
+          (λ _ x↝y → x↝y)
+          (λ y↝z _ _ y-nf _ → absurd (y-nf (_ , y↝z)))
+          hlevel!
+          y↝w y-nf x↝w)
+    (confluent→church-rosser conf x↔y)
+```
+
+Furthermore, if $R$ is a confluent relation on a set, and $x y : A$
+are convertible normal forms, then $x = y$. This follows via a
+straight-forward induction on the wedge produced via confluence.
+
+```agda
+confluent+convertible→unique-normal-form
+  : ∀ {R : Rel A A ℓ} {x y}
+  → is-set A
+  → is-confluent R
+  → Refl-sym-trans R x y
+  → is-normal-form R x → is-normal-form R y
+  → x ≡ y
+confluent+convertible→unique-normal-form {R = R} set conf x↔y x-nf y-nf =
+  ∥-∥-rec (set _ _)
+    (λ where
+      (w , x↝w , y↝w) →
+        Refl-trans-case-wedge
+          (λ x y w → is-normal-form R x → is-normal-form R y → x ≡ y)
+          (λ _ _ → refl)
+          (λ y↝y' _ _ y-nf → absurd (y-nf (_ , y↝y')))
+          (λ x↝x' _ x-nf _ → absurd (x-nf (_ , x↝x')))
+          (Π-is-hlevel² 1 λ _ _ → set _ _)
+          x↝w y↝w x-nf y-nf)
+    (confluent→church-rosser conf x↔y)
+```
+
+We can also show that if $R$ is a confluent relation on a set, and
+$x$ and $y$ are convertible, then the their types of normal forms are
+equivalent.
+
+```agda
+confluent+convertible→normal-form-equiv
+  : ∀ {R : Rel A A ℓ} {x y}
+  → is-set A
+  → is-confluent R
+  → Refl-sym-trans R x y
+  → Normal-form R x ≃ Normal-form R y
+confluent+convertible→normal-form-equiv {R = R} {x = x} {y = y} set conf x↔y =
+  ∥-∥-rec!
+    (λ where
+      (w , x↝w , y↝w) →
+        prop-ext!
+          (confluent+wedge+normal-form→normal-form conf x↝w y↝w)
+          (confluent+wedge+normal-form→normal-form conf y↝w x↝w))
+    (confluent→church-rosser conf x↔y)
+  where
+    instance
+      _ : ∀ {x} {n} → H-Level (Normal-form R x) (suc n)
+      _ = H-Level-confluent-normal-form set conf
+```
+
+
 ## Local Confluence and Newman's Lemma
 
 Proving confluence can be difficult, as it requires looking at

From ebb1721a528c98ca89542091b0e94375a2676577 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Sat, 1 Jul 2023 09:25:07 -0700
Subject: [PATCH 17/19] def: some more theorems about normal forms

---
 src/Rewriting/Base.lagda.md      | 18 ++++++++-
 src/Rewriting/Confluent.lagda.md | 63 +++++++++++++++++++++-----------
 2 files changed, 59 insertions(+), 22 deletions(-)

diff --git a/src/Rewriting/Base.lagda.md b/src/Rewriting/Base.lagda.md
index bee74e411..8999a2729 100644
--- a/src/Rewriting/Base.lagda.md
+++ b/src/Rewriting/Base.lagda.md
@@ -167,10 +167,26 @@ normal-form+reduces→path
   → is-normal-form R x
   → Refl-trans R x y
   → x ≡ y
-normal-form+reduces→path {R = R} A-set =
+normal-form+reduces→path A-set =
   Refl-trans-rec-normal-form _≡_ refl (A-set _ _)
 ```
 
+As a corollary, if $x$ and $y$ are normal forms such that
+$x \to^{*} z \leftarrow^{*} y$, then $x = y$.
+
+```agda
+normal-forms+wedge→path
+  : ∀ {R : Rel A A ℓ} {x y z}
+  → is-set A
+  → is-normal-form R x → is-normal-form R y
+  → Refl-trans R x z → Refl-trans R y z
+  → x ≡ y
+normal-forms+wedge→path set x-nf y-nf x↝z y↝z =
+  normal-form+reduces→path set x-nf x↝z
+  ∙ (sym $ normal-form+reduces→path set y-nf y↝z)
+```
+
+
 <!-- [TODO: Reed M, 28/06/2023] Prove that this yields a pointed identity system -->
 
 If $x$ is a normal form, and $x \to^{*} z$ and $y \to^{*} z$, then
diff --git a/src/Rewriting/Confluent.lagda.md b/src/Rewriting/Confluent.lagda.md
index 7210a3fec..17cef9ba7 100644
--- a/src/Rewriting/Confluent.lagda.md
+++ b/src/Rewriting/Confluent.lagda.md
@@ -108,6 +108,36 @@ refl-trans-clo-equiv+confluent→confluent eqv R-conf {x} {y} {z} =
 If a rewrite system on a set is confluent, then every element of $A$
 has at most one normal form.
 
+To show this, assume that $y$ and $z$ are both normal forms of $x$.
+This gives us the following fork:
+
+~~~{.quiver}
+\begin{tikzcd}
+  & x \\
+  y && z
+  \arrow["{*}"', from=1-2, to=2-1]
+  \arrow["{*}", from=1-2, to=2-3]
+\end{tikzcd}
+~~~
+
+We can apply confluence to obtain a wedge $y \to^{*} w \leftarrow^{*} z$.
+
+~~~{.quiver}
+\begin{tikzcd}
+  & x \\
+  y && z \\
+  & w
+  \arrow["{*}"', from=1-2, to=2-1]
+  \arrow["{*}", from=1-2, to=2-3]
+  \arrow["{*}"', from=2-1, to=3-2]
+  \arrow["{*}", from=2-3, to=3-2]
+  \arrow["Conf"{description}, color={rgb,255:red,92;green,92;blue,214}, draw=none, from=1-2, to=3-2]
+\end{tikzcd}
+~~~
+
+Both $y$ and $z$ are normal forms, so this gives us a pair of paths $y = w$ and
+$z = w$, which completes the proof.
+
 ```agda
 confluent→unique-normal-forms
   : ∀ {R : Rel A A ℓ}
@@ -115,16 +145,14 @@ confluent→unique-normal-forms
   → is-confluent R 
   → ∀ x → is-prop (Normal-form R x)
 confluent→unique-normal-forms {R = R} A-set conf x y-nf z-nf =
-  ∥-∥-proj (Normal-form-is-hlevel 0 A-set y-nf z-nf) $ do
-    w , y↝w , z↝w ← conf (y-nf .reduces) (z-nf .reduces)
-    p ← Refl-trans-case-wedge
-         (λ y z w → is-normal-form R y → is-normal-form R z → ∥ y ≡ z ∥)
-         (λ _ _ → inc refl)
-         (λ z→z' _ _ z-nf → absurd (z-nf (_ , z→z')))
-         (λ y→y' _ y-nf _ → absurd (y-nf (_ , y→y')))
-         hlevel!
-         y↝w z↝w (y-nf .has-normal-form) (z-nf .has-normal-form)
-    pure (Normal-form-path y-nf z-nf p)
+  ∥-∥-rec (Normal-form-is-hlevel 0 A-set y-nf z-nf)
+    (λ where
+      (w , y↝w , z↝w) →
+        Normal-form-path y-nf z-nf
+          (normal-forms+wedge→path A-set
+            (y-nf .has-normal-form) (z-nf .has-normal-form)
+            y↝w z↝w))
+    (conf (y-nf .reduces) (z-nf .reduces))
 ```
 
 <!--
@@ -479,8 +507,8 @@ confluent+convertible→reduces-to-normal-form {R = R} {x = x} {y = y} conf x↔
 ```
 
 Furthermore, if $R$ is a confluent relation on a set, and $x y : A$
-are convertible normal forms, then $x = y$. This follows via a
-straight-forward induction on the wedge produced via confluence.
+are convertible normal forms, then $x = y$. This follows from
+`normal-forms+wedge→path`{.Agda} and confluence.
 
 ```agda
 confluent+convertible→unique-normal-form
@@ -490,17 +518,11 @@ confluent+convertible→unique-normal-form
   → Refl-sym-trans R x y
   → is-normal-form R x → is-normal-form R y
   → x ≡ y
-confluent+convertible→unique-normal-form {R = R} set conf x↔y x-nf y-nf =
+confluent+convertible→unique-normal-form set conf x↔y x-nf y-nf =
   ∥-∥-rec (set _ _)
     (λ where
       (w , x↝w , y↝w) →
-        Refl-trans-case-wedge
-          (λ x y w → is-normal-form R x → is-normal-form R y → x ≡ y)
-          (λ _ _ → refl)
-          (λ y↝y' _ _ y-nf → absurd (y-nf (_ , y↝y')))
-          (λ x↝x' _ x-nf _ → absurd (x-nf (_ , x↝x')))
-          (Π-is-hlevel² 1 λ _ _ → set _ _)
-          x↝w y↝w x-nf y-nf)
+        normal-forms+wedge→path set x-nf y-nf x↝w y↝w)
     (confluent→church-rosser conf x↔y)
 ```
 
@@ -529,7 +551,6 @@ confluent+convertible→normal-form-equiv {R = R} {x = x} {y = y} set conf x↔y
       _ = H-Level-confluent-normal-form set conf
 ```
 
-
 ## Local Confluence and Newman's Lemma
 
 Proving confluence can be difficult, as it requires looking at

From 48d99397a263777c50e5098d92a40cc610715173 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Sat, 1 Jul 2023 09:25:36 -0700
Subject: [PATCH 18/19] fix: clean up unused files

---
 src/Data/Rel/Confluent.lagda.md | 77 ---------------------------------
 1 file changed, 77 deletions(-)
 delete mode 100644 src/Data/Rel/Confluent.lagda.md

diff --git a/src/Data/Rel/Confluent.lagda.md b/src/Data/Rel/Confluent.lagda.md
deleted file mode 100644
index 6c715da01..000000000
--- a/src/Data/Rel/Confluent.lagda.md
+++ /dev/null
@@ -1,77 +0,0 @@
-<!--
-```agda
-open import 1Lab.Prelude
-
-open import Data.Rel.Closure
-```
--->
-
-```agda
-module Data.Rel.Confluent where
-```
-
-# Confluence
-
-<!--
-```agda
-private variable
-  ℓ ℓ' ℓ'' : Level
-  A B X : Type ℓ
-  R : A → A → Type ℓ
-```
--->
-
-```agda
-has-church-rosser : (A → A → Type ℓ) → Type _
-has-church-rosser {A = A} R =
-  ∀ {x y} → Refl-sym-trans R x y
-  → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z)
-
-is-confluent : (A → A → Type ℓ) → Type _
-is-confluent {A = A} R =
-  ∀ {a x y} → Refl-trans R a x → Refl-trans R a y
-  → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z)
-
-is-semi-confluent : (A → A → Type ℓ) → Type _
-is-semi-confluent {A = A} R =
-  ∀ {a x y} → Refl-trans R a x → R a y
-  → ∃[ z ∈ A ] (Refl-trans R x z × Refl-trans R y z)
-
-church-rosser→confluent : has-church-rosser R → is-confluent R
-church-rosser→confluent church-rosser r+ s+ =
-  church-rosser $
-    transitive
-      (symmetric (refl-trans→refl-sym-trans r+))
-      (refl-trans→refl-sym-trans s+)
-
-semiconfluent→church-rosser : is-semi-confluent R → has-church-rosser R
-semiconfluent→church-rosser {R = R} semiconf r+ =
-  Refl-sym-trans-rec-length
-    (λ x y →  ∃[ z ∈ _ ] (Refl-trans R x z × Refl-trans R y z))
-    (inc (_ , reflexive , reflexive))
-    (λ x~y r+ → do
-      z' , y~z' , z~z' ← r+
-      z'' , z'~z'' , y~z'' ← semiconf (transitive [ x~y ] y~z') x~y
-      pure (z'' , transitive [ x~y ] y~z'' , transitive z~z' z'~z''))
-    (λ y~x r+ → do
-      z' , y~z' , z~z' ← r+
-      z'' , z'~z'' , x~z'' ← semiconf y~z' y~x
-      pure (z'' , x~z'' , transitive z~z' z'~z''))
-    squash
-    r+
-
-confluent→semiconfluent : is-confluent R → is-semi-confluent R
-confluent→semiconfluent conf r+ s = conf r+ [ s ]
-
-semiconfluent→confluent : is-semi-confluent R → is-confluent R
-semiconfluent→confluent conf =
-  church-rosser→confluent (semiconfluent→church-rosser conf)
-
-confluent→church-rosser : is-confluent R → has-church-rosser R
-confluent→church-rosser conf =
-  semiconfluent→church-rosser (confluent→semiconfluent conf)
-
-church-rosser→semiconfluent : has-church-rosser R → is-semi-confluent R
-church-rosser→semiconfluent church-rosser =
-  confluent→semiconfluent (church-rosser→confluent church-rosser)
-```

From bfa4de150f763b76d9aaabfbdcd51907eb704420 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Sat, 1 Jul 2023 09:55:42 -0700
Subject: [PATCH 19/19] fix: fix up links

---
 src/Rewriting/Base.lagda.md                | 2 +-
 src/Rewriting/Commute.lagda.md             | 2 +-
 src/Rewriting/Confluent.lagda.md           | 2 +-
 src/Rewriting/StronglyNormalising.lagda.md | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Rewriting/Base.lagda.md b/src/Rewriting/Base.lagda.md
index 8999a2729..6d38ea9a8 100644
--- a/src/Rewriting/Base.lagda.md
+++ b/src/Rewriting/Base.lagda.md
@@ -32,7 +32,7 @@ rewriting rules. Sequences of rewrites are then described using the
 [reflexive transitive closure] of $\to$.
 
 [relation]: Data.Rel.Base.html
-[reflexive transitive closure]: Data.Rel.Closure.html#reflexive-transitive-closure.html
+[reflexive transitive closure]: Data.Rel.Closure.ReflexiveTransitive.html
 
 ## Basic Concepts
 
diff --git a/src/Rewriting/Commute.lagda.md b/src/Rewriting/Commute.lagda.md
index db19681cb..12cb63bd6 100644
--- a/src/Rewriting/Commute.lagda.md
+++ b/src/Rewriting/Commute.lagda.md
@@ -55,7 +55,7 @@ from $R$ and $S$ don't let us diverge; we can always reconcile the two
 by performing rewrites from $S$ and $R$, resp. This generalizes
 [confluence], which states that a relation commutes with itself.
 
-[confluence]: Rewriting.Confluence.html
+[confluence]: Rewriting.Confluent.html
 
 This condition can be somewhat difficult to work with, so we introduce
 an intermediate notion of **semi-commutation**, where one of the reflexive
diff --git a/src/Rewriting/Confluent.lagda.md b/src/Rewriting/Confluent.lagda.md
index 17cef9ba7..b8b580f0a 100644
--- a/src/Rewriting/Confluent.lagda.md
+++ b/src/Rewriting/Confluent.lagda.md
@@ -232,7 +232,7 @@ a variant of confluence known as the **Church-Rosser Property**, which
 requires a $z$ for every pair of equivalent terms $x$ and $y$ such that
 $x \to^{*} z$ and $y \to^{*} z$.
 
-[reflexive symmetric transitive closure]: Data.Rel.Closure.html#reflexive-symmetric-transitive-closure.html
+[reflexive symmetric transitive closure]: Data.Rel.Closure.ReflexiveSymmetricTransitive.html
 
 ~~~{.quiver}
 \begin{tikzcd}
diff --git a/src/Rewriting/StronglyNormalising.lagda.md b/src/Rewriting/StronglyNormalising.lagda.md
index 02f281549..58d614ff2 100644
--- a/src/Rewriting/StronglyNormalising.lagda.md
+++ b/src/Rewriting/StronglyNormalising.lagda.md
@@ -24,7 +24,7 @@ private variable
 An abstract rewriting system is **strongly normalising** if its
 [transitive closure] is a [well-founded relation].
 
-[transitive closure]: Data.Rel.Closure.html#transitive-closure
+[transitive closure]: Data.Rel.Closure.Transitive.html
 [well-founded relation]: Data.Wellfounded.Base.html
 
 ```agda