From 5619f17b4a2d22c1da649591f412f68322873790 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 21 Jun 2025 15:46:14 +0100
Subject: [PATCH 01/21] add: lemmas for decidable equality on `Fin`, plus
 backport to `Nat`

---
 CHANGELOG.md                 | 13 ++++++++++++-
 src/Data/Fin/Properties.agda | 13 ++++++++++++-
 src/Data/Nat/Properties.agda |  3 +++
 3 files changed, 27 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9a75fdaee8..16e8093aa8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -237,13 +237,19 @@ Additions to existing modules
   ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
   ```
 
+* In `Data.Fin.Properties`:
+  ```agda
+  ≡-irrelevant : Irrelevant {A = Fin n} _≡_
+  ≟-diag       : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
+  ≟-diag-refl  : (i : Fin n) → (i ≟ i) ≡ yes refl
+  ```
+
 * In `Data.Fin.Subset`:
   ```agda
   _⊇_ : Subset n → Subset n → Set
   _⊉_ : Subset n → Subset n → Set
   _⊃_ : Subset n → Subset n → Set
   _⊅_ : Subset n → Subset n → Set
-
   ```
 
 * In `Data.Fin.Subset.Induction`:
@@ -278,6 +284,11 @@ Additions to existing modules
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
 
+* In `Data.Nat.Properties`:
+  ```agda
+  ≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl
+  ```
+
 * In `Data.Product.Function.Dependent.Propositional`:
   ```agda
   Σ-↪ : (I↪J : I ↪ J) → (∀ {j} → A (from I↪J j) ↪ B j) → Σ I A ↪ Σ J B
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index e1f2d25d24..c5dffe54a9 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -11,6 +11,7 @@
 module Data.Fin.Properties where
 
 open import Axiom.Extensionality.Propositional
+open import Axiom.UniquenessOfIdentityProofs using (module Decidable⇒UIP)
 open import Algebra.Definitions using (Involutive)
 open import Effect.Applicative using (RawApplicative)
 open import Effect.Functor using (RawFunctor)
@@ -44,10 +45,11 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_)
 open import Relation.Binary.PropositionalEquality.Properties as ≡
   using (module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality using (≡-≟-identity)
 open import Relation.Nullary.Decidable as Dec
   using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
-open import Relation.Nullary.Reflects using (Reflects; invert)
+open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary as U
   using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
 open import Relation.Unary.Properties using (U?)
@@ -100,6 +102,15 @@ zero  ≟ suc y = no λ()
 suc x ≟ zero  = no λ()
 suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y)
 
+≡-irrelevant : Irrelevant {A = Fin n} _≡_
+≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_
+
+≟-diag : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
+≟-diag = ≡-≟-identity _≟_
+
+≟-diag-refl : (i : Fin n)  → (i ≟ i) ≡ yes refl
+≟-diag-refl _ = ≟-diag refl
+
 ------------------------------------------------------------------------
 -- Structures
 
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 5cadc91273..309d530257 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -110,6 +110,9 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≟-diag : (eq : m ≡ n) → (m ≟ n) ≡ yes eq
 ≟-diag = ≡-≟-identity _≟_
 
+≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl
+≟-diag-refl _ = ≟-diag refl
+
 ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ})
 ≡-isDecEquivalence = record
   { isEquivalence = isEquivalence

From 84c94202277315cdb015f450496267f8d5cf2073 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 21 Jun 2025 15:46:43 +0100
Subject: [PATCH 02/21] refactor: knock-ons

---
 src/Data/Fin/Permutation.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 794b93f76b..885dfdfac4 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -12,7 +12,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut)
 open import Data.Fin.Patterns using (0F)
 open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn;
-  punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0)
+  punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0; ≟-diag-refl)
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero)
 open import Data.Product.Base using (_,_; proj₂)
@@ -197,7 +197,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 
   inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ k with i ≟ k
-  ... | yes i≡k rewrite proj₂ (dec-yes (j ≟ j) refl) = i≡k
+  ... | yes i≡k rewrite ≟-diag-refl j = i≡k
   ... | no  i≢k
     with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym
     rewrite dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) j≢punchInⱼπʳpunchOuti≢k
@@ -210,7 +210,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ k with j ≟ k
-  ... | yes j≡k rewrite proj₂ (dec-yes (i ≟ i) refl) = j≡k
+  ... | yes j≡k rewrite ≟-diag-refl i = j≡k
   ... | no  j≢k
     with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym
     rewrite dec-no (i ≟ punchIn i (π ⟨$⟩ˡ punchOut j≢k)) i≢punchInᵢπˡpunchOutj≢k

From 8ad7b41febb166ec94dda6fdd26a0e9c6b497201 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 21 Jun 2025 15:53:38 +0100
Subject: [PATCH 03/21] fix: `import`s

---
 src/Data/Fin/Permutation.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 885dfdfac4..20d0a7ca3f 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -26,7 +26,7 @@ open import Function.Base using (_∘_)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary using (does; ¬_; yes; no)
-open import Relation.Nullary.Decidable using (dec-yes; dec-no)
+open import Relation.Nullary.Decidable using (dec-no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂)

From c781fc18e2269c72854fc954f444b9e23c7e8eb9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 22 Jun 2025 08:46:29 +0100
Subject: [PATCH 04/21] tighten up

---
 src/Data/Fin/Properties.agda | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index c5dffe54a9..6610ca2d3b 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -45,7 +45,8 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_)
 open import Relation.Binary.PropositionalEquality.Properties as ≡
   using (module ≡-Reasoning)
-open import Relation.Binary.PropositionalEquality using (≡-≟-identity)
+open import Relation.Binary.PropositionalEquality as ≡
+  using (≡-≟-identity)
 open import Relation.Nullary.Decidable as Dec
   using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)

From 5279af11bb5fce3d4fa4b85552fe78a910d72572 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 22 Jun 2025 08:47:59 +0100
Subject: [PATCH 05/21] refactor: add new lemmas, simplify old proof

---
 CHANGELOG.md                             |  8 ++++
 src/Data/Fin/Permutation/Components.agda | 49 ++++++++++++++----------
 2 files changed, 36 insertions(+), 21 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 16e8093aa8..49071c07cb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -237,6 +237,14 @@ Additions to existing modules
   ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
   ```
 
+* In `Data.Fin.Permutation.Components`:
+  ```agda
+  transpose-iij : (i j : Fin n) → transpose i i j ≡ j
+  transpose-ijj : (i j : Fin n) → transpose i j j ≡ i
+  transpose-iji : (i j : Fin n) → transpose i j i ≡ j
+  transpose-transpose : transpose i j k ≡ l → transpose j i l ≡ k
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   ≡-irrelevant : Irrelevant {A = Fin n} _≡_
diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda
index 2d2f34deb7..6a4ad9e6b9 100644
--- a/src/Data/Fin/Permutation/Components.agda
+++ b/src/Data/Fin/Permutation/Components.agda
@@ -11,25 +11,18 @@ module Data.Fin.Permutation.Components where
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Fin.Base using (Fin; suc; opposite; toℕ)
 open import Data.Fin.Properties
-  using (_≟_; opposite-prop; opposite-involutive; opposite-suc)
-open import Data.Nat.Base as ℕ using (zero; suc; _∸_)
-open import Data.Product.Base using (proj₂)
-open import Function.Base using (_∘_)
+  using (_≟_; ≟-diag; ≟-diag-refl
+        ; opposite-prop; opposite-involutive; opposite-suc)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (does; _because_; yes; no)
-open import Relation.Nullary.Decidable using (dec-true; dec-false)
+open import Relation.Nullary.Decidable.Core using (does; _because_)
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; sym; trans)
-open import Relation.Binary.PropositionalEquality.Properties
-  using (module ≡-Reasoning)
-open import Algebra.Definitions using (Involutive)
-open ≡-Reasoning
+  using (_≡_; refl; sym)
 
 ------------------------------------------------------------------------
 --  Functions
 ------------------------------------------------------------------------
 
--- 'tranpose i j' swaps the places of 'i' and 'j'.
+-- 'transpose i j' swaps the places of 'i' and 'j'.
 
 transpose : ∀ {n} → Fin n → Fin n → Fin n → Fin n
 transpose i j k with does (k ≟ i)
@@ -42,17 +35,31 @@ transpose i j k with does (k ≟ i)
 --  Properties
 ------------------------------------------------------------------------
 
+transpose-iij : ∀ {n} (i j : Fin n) → transpose i i j ≡ j
+transpose-iij i j with j ≟ i in j≟i
+... | true  because [j≡i] = sym (invert [j≡i])
+... | false because _ rewrite j≟i = refl
+
+transpose-ijj : ∀ {n} (i j : Fin n) → transpose i j j ≡ i
+transpose-ijj i j with j ≟ i
+... | true  because [j≡i] = invert [j≡i]
+... | false because _ rewrite ≟-diag-refl j = refl
+
+transpose-iji : ∀ {n} (i j : Fin n) → transpose i j i ≡ j
+transpose-iji i j rewrite ≟-diag-refl i = refl
+
+transpose-transpose : ∀ {n} {i j k l : Fin n} →
+                      transpose i j k ≡ l → transpose j i l ≡ k
+transpose-transpose {n} {i} {j} {k} {l} eq with k ≟ i in k≟i
+... | true  because [k≡i] rewrite ≟-diag (sym eq) = sym (invert [k≡i])
+... | false because [k≢i] with k ≟ j in k≟j
+...   | true  because [k≡j] rewrite eq | transpose-ijj j l = sym (invert [k≡j])
+...   | false because [k≢j] rewrite eq | k≟j | k≟i = refl
+
 transpose-inverse : ∀ {n} (i j : Fin n) {k} →
                     transpose i j (transpose j i k) ≡ k
-transpose-inverse i j {k} with k ≟ j
-... | true  because [k≡j] rewrite dec-true (i ≟ i) refl = sym (invert [k≡j])
-... | false because [k≢j] with k ≟ i
-...   | true  because [k≡i]
-        rewrite dec-false (j ≟ i) (invert [k≢j] ∘ trans (invert [k≡i]) ∘ sym)
-                | dec-true (j ≟ j) refl
-                = sym (invert [k≡i])
-...   | false because [k≢i] rewrite dec-false (k ≟ i) (invert [k≢i])
-                                  | dec-false (k ≟ j) (invert [k≢j]) = refl
+transpose-inverse i j = transpose-transpose refl
+
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES

From 61da9a62b98dacde5736b6fca8b8692fb22a3a75 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 22 Jun 2025 10:52:03 +0100
Subject: [PATCH 06/21] refactor: additional instantiated lemmas

---
 CHANGELOG.md                 | 1 +
 src/Data/Fin/Properties.agda | 6 +++++-
 src/Data/Nat/Properties.agda | 3 +++
 3 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 49071c07cb..f94f1434a5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -250,6 +250,7 @@ Additions to existing modules
   ≡-irrelevant : Irrelevant {A = Fin n} _≡_
   ≟-diag       : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
   ≟-diag-refl  : (i : Fin n) → (i ≟ i) ≡ yes refl
+  ≟-off-diag : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
   ```
 
 * In `Data.Fin.Subset`:
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 6610ca2d3b..ba3a534f1d 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -46,7 +46,7 @@ open import Relation.Binary.PropositionalEquality.Core as ≡
 open import Relation.Binary.PropositionalEquality.Properties as ≡
   using (module ≡-Reasoning)
 open import Relation.Binary.PropositionalEquality as ≡
-  using (≡-≟-identity)
+  using (≡-≟-identity; ≢-≟-identity)
 open import Relation.Nullary.Decidable as Dec
   using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
@@ -112,6 +112,10 @@ suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y)
 ≟-diag-refl : (i : Fin n)  → (i ≟ i) ≡ yes refl
 ≟-diag-refl _ = ≟-diag refl
 
+≟-off-diag : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
+≟-off-diag = ≢-≟-identity _≟_
+
+
 ------------------------------------------------------------------------
 -- Structures
 
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 309d530257..3e93abcfb5 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -113,6 +113,9 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl
 ≟-diag-refl _ = ≟-diag refl
 
+≟-off-diag : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
+≟-off-diag = ≢-≟-identity _≟_
+
 ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ})
 ≡-isDecEquivalence = record
   { isEquivalence = isEquivalence

From 5c1c29e2b09f63a8200215e35e48daa2e202cf14 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 22 Jun 2025 10:57:41 +0100
Subject: [PATCH 07/21] refactor: further streamlining of proofs and `import`s

---
 src/Data/Fin/Permutation.agda | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 20d0a7ca3f..63fbff0bf7 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -11,11 +11,13 @@ module Data.Fin.Permutation where
 open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut)
 open import Data.Fin.Patterns using (0F)
-open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn;
-  punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0; ≟-diag-refl)
+open import Data.Fin.Properties
+  using (¬Fin0; _≟_; ≟-diag-refl; ≟-off-diag
+        ; punchInᵢ≢i; punchOut-punchIn; punchIn-punchOut
+        ; punchOut-cong; punchOut-cong′)
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero)
-open import Data.Product.Base using (_,_; proj₂)
+open import Data.Product.Base using (_,_)
 open import Function.Bundles using (_↔_; Injection; Inverse; mk↔ₛ′)
 open import Function.Construct.Composition using (_↔-∘_)
 open import Function.Construct.Identity using (↔-id)
@@ -25,9 +27,8 @@ open import Function.Properties.Inverse using (↔⇒↣)
 open import Function.Base using (_∘_)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Nullary using (does; ¬_; yes; no)
-open import Relation.Nullary.Decidable using (dec-no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂)
 open import Relation.Binary.PropositionalEquality.Properties
@@ -200,7 +201,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
   ... | yes i≡k rewrite ≟-diag-refl j = i≡k
   ... | no  i≢k
     with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym
-    rewrite dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) j≢punchInⱼπʳpunchOuti≢k
+    rewrite ≟-off-diag j≢punchInⱼπʳpunchOuti≢k
     = begin
     punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩
     punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩
@@ -213,7 +214,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
   ... | yes j≡k rewrite ≟-diag-refl i = j≡k
   ... | no  j≢k
     with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym
-    rewrite dec-no (i ≟ punchIn i (π ⟨$⟩ˡ punchOut j≢k)) i≢punchInᵢπˡpunchOutj≢k
+    rewrite ≟-off-diag i≢punchInᵢπˡpunchOutj≢k
     = begin
     punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
     punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
@@ -296,9 +297,7 @@ insert-remove {m = m} {n = n} i π j with i ≟ j
   π ⟨$⟩ʳ j ∎
 
 remove-insert : ∀ i j (π : Permutation m n) → remove i (insert i j π) ≈ π
-remove-insert i j π k with i ≟ i
-... | no i≢i = contradiction refl i≢i
-... | yes _ = begin
+remove-insert i j π k rewrite ≟-diag-refl i = begin
   punchOut {i = j} _
     ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩
   punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym)

From 1df6eef74431c07a7b242bb34de592825eb7a78e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 22 Jun 2025 10:58:49 +0100
Subject: [PATCH 08/21] `CHANGELOG`

---
 CHANGELOG.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f94f1434a5..66fc571ede 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -250,7 +250,7 @@ Additions to existing modules
   ≡-irrelevant : Irrelevant {A = Fin n} _≡_
   ≟-diag       : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
   ≟-diag-refl  : (i : Fin n) → (i ≟ i) ≡ yes refl
-  ≟-off-diag : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
+  ≟-off-diag   : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
   ```
 
 * In `Data.Fin.Subset`:
@@ -296,6 +296,7 @@ Additions to existing modules
 * In `Data.Nat.Properties`:
   ```agda
   ≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl
+  ≟-off-diag  : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
   ```
 
 * In `Data.Product.Function.Dependent.Propositional`:

From 4f4be18607e7d8c1f2bb0e80995d8bae2b5ba84e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 22 Jun 2025 11:33:47 +0100
Subject: [PATCH 09/21] whitespace

---
 src/Data/Fin/Properties.agda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index ba3a534f1d..846a3ba8c0 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -115,7 +115,6 @@ suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y)
 ≟-off-diag : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
 ≟-off-diag = ≢-≟-identity _≟_
 
-
 ------------------------------------------------------------------------
 -- Structures
 

From 842a3bbb98a932fab4f2e5181a9e6346de6ccb38 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 24 Jun 2025 10:35:30 +0100
Subject: [PATCH 10/21] fix: #2743

---
 src/Data/Fin/Permutation/Components.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda
index 6a4ad9e6b9..4f38ab0da6 100644
--- a/src/Data/Fin/Permutation/Components.agda
+++ b/src/Data/Fin/Permutation/Components.agda
@@ -76,20 +76,20 @@ Please use opposite from Data.Fin.Base instead."
 #-}
 
 reverse-prop = opposite-prop
-{-# WARNING_ON_USAGE reverse
+{-# WARNING_ON_USAGE reverse-prop
 "Warning: reverse-prop was deprecated in v2.0.
 Please use opposite-prop from Data.Fin.Properties instead."
 #-}
 
 reverse-involutive = opposite-involutive
-{-# WARNING_ON_USAGE reverse
+{-# WARNING_ON_USAGE reverse-involutive
 "Warning: reverse-involutive was deprecated in v2.0.
 Please use opposite-involutive from Data.Fin.Properties instead."
 #-}
 
 reverse-suc : ∀ {n} {i : Fin n} → toℕ (opposite (suc i)) ≡ toℕ (opposite i)
 reverse-suc {i = i} = opposite-suc i
-{-# WARNING_ON_USAGE reverse
+{-# WARNING_ON_USAGE reverse-suc
 "Warning: reverse-suc was deprecated in v2.0.
 Please use opposite-suc from Data.Fin.Properties instead."
 #-}

From 5373f2f7502ac417772ead86ee67f551da2d7c2c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 24 Jun 2025 10:56:19 +0100
Subject: [PATCH 11/21] fix: deprecation bug

---
 src/Data/Fin/Permutation.agda | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 63fbff0bf7..359e96f745 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -13,6 +13,7 @@ open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut)
 open import Data.Fin.Patterns using (0F)
 open import Data.Fin.Properties
   using (¬Fin0; _≟_; ≟-diag-refl; ≟-off-diag
+        ; opposite-involutive
         ; punchInᵢ≢i; punchOut-punchIn; punchIn-punchOut
         ; punchOut-cong; punchOut-cong′)
 import Data.Fin.Permutation.Components as PC
@@ -98,7 +99,7 @@ transpose i j = permutation (PC.transpose i j) (PC.transpose j i) (λ _ → PC.t
 -- Reverse the order of indices
 
 reverse : Permutation′ n
-reverse = permutation opposite opposite PC.reverse-involutive PC.reverse-involutive
+reverse = permutation opposite opposite opposite-involutive opposite-involutive
 
 ------------------------------------------------------------------------
 -- Operations

From e966871038ad15744fc479923777ae67d38433f8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 24 Jun 2025 11:42:37 +0100
Subject: [PATCH 12/21] fix: equational reaosning layout

---
 src/Data/Fin/Permutation.agda | 74 +++++++++++++++++++++++------------
 1 file changed, 48 insertions(+), 26 deletions(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 359e96f745..dface3cf2a 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -147,19 +147,27 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
 
   inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ j = begin
-    from (to j)                                                      ≡⟨⟩
-    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩
-    punchOut {i = i} {πˡ (πʳ (punchIn i j))}                      _  ≡⟨ punchOut-cong i (inverseˡ π) ⟩
-    punchOut {i = i} {punchIn i j}                                _  ≡⟨ punchOut-punchIn i ⟩
-    j                                                                ∎
+    from (to j)
+      ≡⟨⟩
+    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _
+      ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩
+    punchOut {i = i} {πˡ (πʳ (punchIn i j))}                      _
+      ≡⟨ punchOut-cong i (inverseˡ π) ⟩
+    punchOut {i = i} {punchIn i j}                                _
+      ≡⟨ punchOut-punchIn i ⟩
+    j ∎
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ j = begin
-    to (from j)                                                       ≡⟨⟩
-    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _  ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩
-    punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _  ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
-    punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _  ≡⟨ punchOut-punchIn (πʳ i) ⟩
-    j                                                                 ∎
+    to (from j)
+      ≡⟨⟩
+    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _
+      ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩
+    punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _
+      ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
+    punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _
+      ≡⟨ punchOut-punchIn (πʳ i) ⟩
+    j ∎
 
 -- lift: takes a permutation m → n and creates a permutation (suc m) → (suc n)
 -- by mapping 0 to 0 and applying the input permutation to everything else
@@ -204,11 +212,15 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym
     rewrite ≟-off-diag j≢punchInⱼπʳpunchOuti≢k
     = begin
-    punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩
-    punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩
-    punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k))                              ≡⟨ cong (punchIn i) (inverseˡ π) ⟩
-    punchIn i (punchOut i≢k)                                              ≡⟨ punchIn-punchOut i≢k ⟩
-    k                                                                     ∎
+    punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)
+      ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩
+    punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym))
+      ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩
+    punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k))
+      ≡⟨ cong (punchIn i) (inverseˡ π) ⟩
+    punchIn i (punchOut i≢k)
+      ≡⟨ punchIn-punchOut i≢k ⟩
+    k ∎
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ k with j ≟ k
@@ -217,11 +229,15 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym
     rewrite ≟-off-diag i≢punchInᵢπˡpunchOutj≢k
     = begin
-    punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
-    punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
-    punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k))                               ≡⟨ cong (punchIn j) (inverseʳ π) ⟩
-    punchIn j (punchOut j≢k)                                               ≡⟨ punchIn-punchOut j≢k ⟩
-    k                                                                      ∎
+    punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)
+      ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
+    punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym))
+      ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
+    punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k))
+      ≡⟨ cong (punchIn j) (inverseʳ π) ⟩
+    punchIn j (punchOut j≢k)
+      ≡⟨ punchIn-punchOut j≢k ⟩
+    k ∎
 
 ------------------------------------------------------------------------
 -- Other properties
@@ -285,17 +301,23 @@ insert-punchIn : ∀ i j (π : Permutation m n) k → insert i j π ⟨$⟩ʳ pu
 insert-punchIn i j π k with i ≟ punchIn i k
 ... | yes i≡punchInᵢk = contradiction (sym i≡punchInᵢk) (punchInᵢ≢i i k)
 ... | no  i≢punchInᵢk = begin
-  punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢk)            ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
-  punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i k ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
-  punchIn j (π ⟨$⟩ʳ k)                               ∎
+  punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢk)
+    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
+  punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i k ∘ sym))
+    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
+  punchIn j (π ⟨$⟩ʳ k)
+    ∎
 
 insert-remove : ∀ i (π : Permutation (suc m) (suc n)) → insert i (π ⟨$⟩ʳ i) (remove i π) ≈ π
 insert-remove {m = m} {n = n} i π j with i ≟ j
 ... | yes i≡j = cong (π ⟨$⟩ʳ_) i≡j
 ... | no  i≢j = begin
-  punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π))) ≡⟨ punchIn-punchOut _ ⟩
-  π ⟨$⟩ʳ punchIn i (punchOut i≢j) ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩
-  π ⟨$⟩ʳ j ∎
+  punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π)))
+    ≡⟨ punchIn-punchOut _ ⟩
+  π ⟨$⟩ʳ punchIn i (punchOut i≢j)
+    ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩
+  π ⟨$⟩ʳ j
+    ∎
 
 remove-insert : ∀ i j (π : Permutation m n) → remove i (insert i j π) ≈ π
 remove-insert i j π k rewrite ≟-diag-refl i = begin

From 075efe3c80c468a0d8b3abb83453a5d379352520 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 26 Jun 2025 07:44:09 +0100
Subject: [PATCH 13/21] fix: merge conflicts

---
 src/Data/Fin/Permutation.agda | 22 +++++-----------------
 1 file changed, 5 insertions(+), 17 deletions(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 86c2f00498..b5935f57f1 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -9,20 +9,13 @@
 module Data.Fin.Permutation where
 
 open import Data.Bool.Base using (true; false)
-<<<<<<< refactor-Fin-properties
-open import Data.Fin.Base using (Fin; suc; opposite; punchIn; punchOut)
-open import Data.Fin.Patterns using (0F)
+open import Data.Fin.Base using (Fin; suc; cast; opposite; punchIn; punchOut)
+open import Data.Fin.Patterns using (0F; 1F)
 open import Data.Fin.Properties
   using (¬Fin0; _≟_; ≟-diag-refl; ≟-off-diag
-        ; opposite-involutive
+        ; cast-involutive; opposite-involutive
         ; punchInᵢ≢i; punchOut-punchIn; punchIn-punchOut
         ; punchOut-cong; punchOut-cong′)
-=======
-open import Data.Fin.Base using (Fin; suc; cast; opposite; punchIn; punchOut)
-open import Data.Fin.Patterns using (0F; 1F)
-open import Data.Fin.Properties using (punchInᵢ≢i; punchOut-punchIn;
-  punchOut-cong; punchOut-cong′; punchIn-punchOut; _≟_; ¬Fin0; cast-involutive)
->>>>>>> master
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero)
 open import Data.Product.Base using (_,_)
@@ -106,13 +99,8 @@ flip = ↔-sym
 
 infixr 9 _∘ₚ_
 
-<<<<<<< refactor-Fin-properties
-reverse : Permutation′ n
-reverse = permutation opposite opposite opposite-involutive opposite-involutive
-=======
 _∘ₚ_ : Permutation m n → Permutation n o → Permutation m o
 π₁ ∘ₚ π₂ = π₂ ↔-∘ π₁
->>>>>>> master
 
 ------------------------------------------------------------------------
 -- Non-trivial identity
@@ -144,8 +132,8 @@ reverse : Permutation n n
 reverse = permutation
   opposite
   opposite
-  PC.reverse-involutive
-  PC.reverse-involutive
+  opposite-involutive
+  opposite-involutive
 
 ------------------------------------------------------------------------
 -- Element removal

From c4fe9947e7c222f761e2bb9aa064d1d4f753e28e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 27 Jun 2025 05:06:17 +0100
Subject: [PATCH 14/21] fix: equation alignment

---
 src/Data/Fin/Permutation.agda | 55 ++++++++++++-----------------------
 1 file changed, 19 insertions(+), 36 deletions(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index b5935f57f1..b85c8f0b9f 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -242,15 +242,11 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym
     rewrite ≟-off-diag j≢punchInⱼπʳpunchOuti≢k
     = begin
-    punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)
-      ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩
-    punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym))
-      ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩
-    punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k))
-      ≡⟨ cong (punchIn i) (inverseˡ π) ⟩
-    punchIn i (punchOut i≢k)
-      ≡⟨ punchIn-punchOut i≢k ⟩
-    k ∎
+    punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩
+    punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩
+    punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k))                               ≡⟨ cong (punchIn i) (inverseˡ π) ⟩
+    punchIn i (punchOut i≢k)                                               ≡⟨ punchIn-punchOut i≢k ⟩
+    k                                                                      ∎
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ k with j ≟ k
@@ -259,15 +255,11 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym
     rewrite ≟-off-diag i≢punchInᵢπˡpunchOutj≢k
     = begin
-    punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)
-      ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
-    punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym))
-      ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
-    punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k))
-      ≡⟨ cong (punchIn j) (inverseʳ π) ⟩
-    punchIn j (punchOut j≢k)
-      ≡⟨ punchIn-punchOut j≢k ⟩
-    k ∎
+    punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
+    punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
+    punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k))                               ≡⟨ cong (punchIn j) (inverseʳ π) ⟩
+    punchIn j (punchOut j≢k)                                               ≡⟨ punchIn-punchOut j≢k ⟩
+    k                                                                      ∎
 
 ------------------------------------------------------------------------
 -- Swapping
@@ -343,29 +335,20 @@ insert-punchIn : ∀ i j (π : Permutation m n) k → insert i j π ⟨$⟩ʳ pu
 insert-punchIn i j π k with i ≟ punchIn i k
 ... | yes i≡punchInᵢk = contradiction (sym i≡punchInᵢk) (punchInᵢ≢i i k)
 ... | no  i≢punchInᵢk = begin
-  punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢk)
-    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
-  punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i k ∘ sym))
-    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
-  punchIn j (π ⟨$⟩ʳ k)
-    ∎
+  punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢk)            ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
+  punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i k ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
+  punchIn j (π ⟨$⟩ʳ k)                               ∎
 
 insert-remove : ∀ i (π : Permutation (suc m) (suc n)) → insert i (π ⟨$⟩ʳ i) (remove i π) ≈ π
 insert-remove {m = m} {n = n} i π j with i ≟ j
 ... | yes i≡j = cong (π ⟨$⟩ʳ_) i≡j
 ... | no  i≢j = begin
-  punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π)))
-    ≡⟨ punchIn-punchOut _ ⟩
-  π ⟨$⟩ʳ punchIn i (punchOut i≢j)
-    ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩
-  π ⟨$⟩ʳ j
-    ∎
+  punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π)))                             ≡⟨ punchIn-punchOut _ ⟩
+  π ⟨$⟩ʳ punchIn i (punchOut i≢j)    ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩
+  π ⟨$⟩ʳ j                           ∎
 
 remove-insert : ∀ i j (π : Permutation m n) → remove i (insert i j π) ≈ π
 remove-insert i j π k rewrite ≟-diag-refl i = begin
-  punchOut {i = j} _
-    ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩
-  punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym)
-    ≡⟨ punchOut-punchIn j ⟩
-  π ⟨$⟩ʳ k
-    ∎
+  punchOut {i = j} _                               ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩
+  punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym) ≡⟨ punchOut-punchIn j ⟩
+  π ⟨$⟩ʳ k                                         ∎

From 30ccfa9f0737b8eba587e0c43914c0f2ced99e03 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 27 Jun 2025 05:16:09 +0100
Subject: [PATCH 15/21] fix: equation alignment

---
 src/Data/Fin/Permutation.agda | 28 ++++++++++------------------
 1 file changed, 10 insertions(+), 18 deletions(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index b85c8f0b9f..5f7f3c7728 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -168,27 +168,19 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
 
   inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ j = begin
-    from (to j)
-      ≡⟨⟩
-    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _
-      ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩
-    punchOut {i = i} {πˡ (πʳ (punchIn i j))}                      _
-      ≡⟨ punchOut-cong i (inverseˡ π) ⟩
-    punchOut {i = i} {punchIn i j}                                _
-      ≡⟨ punchOut-punchIn i ⟩
-    j ∎
+    from (to j)                                                     ≡⟨⟩
+    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _ ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩
+    punchOut {i = i} {πˡ (πʳ (punchIn i j))}                      _ ≡⟨ punchOut-cong i (inverseˡ π) ⟩
+    punchOut {i = i} {punchIn i j}                                _ ≡⟨ punchOut-punchIn i ⟩
+    j                                                               ∎
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ j = begin
-    to (from j)
-      ≡⟨⟩
-    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _
-      ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩
-    punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _
-      ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
-    punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _
-      ≡⟨ punchOut-punchIn (πʳ i) ⟩
-    j ∎
+    to (from j)                                                      ≡⟨⟩
+    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _ ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩
+    punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _ ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
+    punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _ ≡⟨ punchOut-punchIn (πʳ i) ⟩
+    j                                                                ∎
 
 ------------------------------------------------------------------------
 -- Lifting

From 8a54c1c4715f54929241aef837d6df8dd4e6c627 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 27 Jun 2025 05:23:10 +0100
Subject: [PATCH 16/21] refactor: `yes` and `no`

---
 src/Data/Fin/Permutation/Components.agda | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda
index 4f38ab0da6..ca9cd9ed19 100644
--- a/src/Data/Fin/Permutation/Components.agda
+++ b/src/Data/Fin/Permutation/Components.agda
@@ -13,8 +13,7 @@ open import Data.Fin.Base using (Fin; suc; opposite; toℕ)
 open import Data.Fin.Properties
   using (_≟_; ≟-diag; ≟-diag-refl
         ; opposite-prop; opposite-involutive; opposite-suc)
-open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary.Decidable.Core using (does; _because_)
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym)
 
@@ -37,13 +36,13 @@ transpose i j k with does (k ≟ i)
 
 transpose-iij : ∀ {n} (i j : Fin n) → transpose i i j ≡ j
 transpose-iij i j with j ≟ i in j≟i
-... | true  because [j≡i] = sym (invert [j≡i])
-... | false because _ rewrite j≟i = refl
+... | yes j≡i           = sym j≡i
+... | no  _ rewrite j≟i = refl
 
 transpose-ijj : ∀ {n} (i j : Fin n) → transpose i j j ≡ i
 transpose-ijj i j with j ≟ i
-... | true  because [j≡i] = invert [j≡i]
-... | false because _ rewrite ≟-diag-refl j = refl
+... | yes j≡i                     = j≡i
+... | no  _ rewrite ≟-diag-refl j = refl
 
 transpose-iji : ∀ {n} (i j : Fin n) → transpose i j i ≡ j
 transpose-iji i j rewrite ≟-diag-refl i = refl
@@ -51,10 +50,10 @@ transpose-iji i j rewrite ≟-diag-refl i = refl
 transpose-transpose : ∀ {n} {i j k l : Fin n} →
                       transpose i j k ≡ l → transpose j i l ≡ k
 transpose-transpose {n} {i} {j} {k} {l} eq with k ≟ i in k≟i
-... | true  because [k≡i] rewrite ≟-diag (sym eq) = sym (invert [k≡i])
-... | false because [k≢i] with k ≟ j in k≟j
-...   | true  because [k≡j] rewrite eq | transpose-ijj j l = sym (invert [k≡j])
-...   | false because [k≢j] rewrite eq | k≟j | k≟i = refl
+... | yes k≡i rewrite ≟-diag (sym eq) = sym k≡i
+... | no k≢i with k ≟ j in k≟j
+...   | yes k≡j rewrite eq | transpose-ijj j l = sym k≡j
+...   | no  k≢j rewrite eq | k≟j | k≟i = refl
 
 transpose-inverse : ∀ {n} (i j : Fin n) {k} →
                     transpose i j (transpose j i k) ≡ k

From f9fc5de905f26ad63e90d5b2a80a2161fc534251 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 30 Jun 2025 08:44:11 +0100
Subject: [PATCH 17/21] fix\; remove Fairbairn violation

---
 CHANGELOG.md                 | 1 -
 src/Data/Nat/Properties.agda | 3 ---
 2 files changed, 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 26fe09d71a..757b86385e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -350,7 +350,6 @@ Additions to existing modules
 
 * In `Data.Nat.Properties`:
   ```agda
-  ≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl
   ≟-off-diag  : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
   ```
 
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 3e93abcfb5..907a215ee8 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -110,9 +110,6 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≟-diag : (eq : m ≡ n) → (m ≟ n) ≡ yes eq
 ≟-diag = ≡-≟-identity _≟_
 
-≟-diag-refl : ∀ n → (n ≟ n) ≡ yes refl
-≟-diag-refl _ = ≟-diag refl
-
 ≟-off-diag : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
 ≟-off-diag = ≢-≟-identity _≟_
 

From 3a5b6cd4fa3644fc5d892a0fae7790a9f0ae62ec Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 3 Jul 2025 07:58:14 +0100
Subject: [PATCH 18/21] rename: `transpose` lemmas

---
 CHANGELOG.md                             |  6 +++---
 src/Data/Fin/Permutation/Components.agda | 14 +++++++-------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 459b84a269..8ba65ea8bf 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -323,9 +323,9 @@ Additions to existing modules
 
 * In `Data.Fin.Permutation.Components`:
   ```agda
-  transpose-iij : (i j : Fin n) → transpose i i j ≡ j
-  transpose-ijj : (i j : Fin n) → transpose i j j ≡ i
-  transpose-iji : (i j : Fin n) → transpose i j i ≡ j
+  transpose[i,i,j]≡j  : (i j : Fin n) → transpose i i j ≡ j
+  transpose[i,j,j]≡i  : (i j : Fin n) → transpose i j j ≡ i
+  transpose[i,j,i]≡j  : (i j : Fin n) → transpose i j i ≡ j
   transpose-transpose : transpose i j k ≡ l → transpose j i l ≡ k
   ```
 
diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda
index ca9cd9ed19..f126906600 100644
--- a/src/Data/Fin/Permutation/Components.agda
+++ b/src/Data/Fin/Permutation/Components.agda
@@ -34,25 +34,25 @@ transpose i j k with does (k ≟ i)
 --  Properties
 ------------------------------------------------------------------------
 
-transpose-iij : ∀ {n} (i j : Fin n) → transpose i i j ≡ j
-transpose-iij i j with j ≟ i in j≟i
+transpose[i,i,j]≡j : ∀ {n} (i j : Fin n) → transpose i i j ≡ j
+transpose[i,i,j]≡j i j with j ≟ i in j≟i
 ... | yes j≡i           = sym j≡i
 ... | no  _ rewrite j≟i = refl
 
-transpose-ijj : ∀ {n} (i j : Fin n) → transpose i j j ≡ i
-transpose-ijj i j with j ≟ i
+transpose[i,j,j]≡i : ∀ {n} (i j : Fin n) → transpose i j j ≡ i
+transpose[i,j,j]≡i i j with j ≟ i
 ... | yes j≡i                     = j≡i
 ... | no  _ rewrite ≟-diag-refl j = refl
 
-transpose-iji : ∀ {n} (i j : Fin n) → transpose i j i ≡ j
-transpose-iji i j rewrite ≟-diag-refl i = refl
+transpose[i,j,i]≡j : ∀ {n} (i j : Fin n) → transpose i j i ≡ j
+transpose[i,j,i]≡j i j rewrite ≟-diag-refl i = refl
 
 transpose-transpose : ∀ {n} {i j k l : Fin n} →
                       transpose i j k ≡ l → transpose j i l ≡ k
 transpose-transpose {n} {i} {j} {k} {l} eq with k ≟ i in k≟i
 ... | yes k≡i rewrite ≟-diag (sym eq) = sym k≡i
 ... | no k≢i with k ≟ j in k≟j
-...   | yes k≡j rewrite eq | transpose-ijj j l = sym k≡j
+...   | yes k≡j rewrite eq | transpose[i,j,j]≡i j l = sym k≡j
 ...   | no  k≢j rewrite eq | k≟j | k≟i = refl
 
 transpose-inverse : ∀ {n} (i j : Fin n) {k} →

From a5b574e6162c8689c4880b09fdb468af647fc40c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 3 Jul 2025 08:05:50 +0100
Subject: [PATCH 19/21] rename: decidable equality lemmas

---
 CHANGELOG.md                 |  8 ++++----
 src/Data/Fin/Properties.agda | 12 ++++++------
 src/Data/Nat/Properties.agda |  4 ++--
 3 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8ba65ea8bf..b47f8dcdf9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -332,9 +332,9 @@ Additions to existing modules
 * In `Data.Fin.Properties`:
   ```agda
   ≡-irrelevant : Irrelevant {A = Fin n} _≡_
-  ≟-diag       : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
-  ≟-diag-refl  : (i : Fin n) → (i ≟ i) ≡ yes refl
-  ≟-off-diag   : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
+  ≟-≡          : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
+  ≟-≡-refl     : (i : Fin n) → (i ≟ i) ≡ yes refl
+  ≟-≢          : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
   cast-involutive       : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k
   inject!-injective     : Injective _≡_ _≡_ inject!
   inject!-<             : (k : Fin′ i) → inject! k < i
@@ -424,7 +424,7 @@ Additions to existing modules
 
 * In `Data.Nat.Properties`:
   ```agda
-  ≟-off-diag  : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
+  ≟-≢  : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
   ```
 
 * In `Data.Product.Function.Dependent.Propositional`:
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index ab76ac8043..f78b652a85 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -106,14 +106,14 @@ suc x ≟ suc y = map′ (cong suc) suc-injective (x ≟ y)
 ≡-irrelevant : Irrelevant {A = Fin n} _≡_
 ≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_
 
-≟-diag : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
-≟-diag = ≡-≟-identity _≟_
+≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
+≟-≡ = ≡-≟-identity _≟_
 
-≟-diag-refl : (i : Fin n)  → (i ≟ i) ≡ yes refl
-≟-diag-refl _ = ≟-diag refl
+≟-≡-refl : (i : Fin n)  → (i ≟ i) ≡ yes refl
+≟-≡-refl _ = ≟-≡ refl
 
-≟-off-diag : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
-≟-off-diag = ≢-≟-identity _≟_
+≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
+≟-≢ = ≢-≟-identity _≟_
 
 ------------------------------------------------------------------------
 -- Structures
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index f639ff8944..7f32b78089 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -114,8 +114,8 @@ m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≟-diag : (eq : m ≡ n) → (m ≟ n) ≡ yes eq
 ≟-diag = ≡-≟-identity _≟_
 
-≟-off-diag : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
-≟-off-diag = ≢-≟-identity _≟_
+≟-≡ : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
+≟-≡ = ≢-≟-identity _≟_
 
 ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ})
 ≡-isDecEquivalence = record

From 4b183660104354852aea8c7d1d9d864a7a9c917a Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 3 Jul 2025 08:11:35 +0100
Subject: [PATCH 20/21] fix: use of new names

---
 src/Data/Fin/Permutation.agda            | 12 ++++++------
 src/Data/Fin/Permutation/Components.agda |  8 ++++----
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 7838763246..5606d3773b 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -12,7 +12,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base using (Fin; suc; cast; opposite; punchIn; punchOut)
 open import Data.Fin.Patterns using (0F; 1F)
 open import Data.Fin.Properties
-  using (¬Fin0; _≟_; ≟-diag-refl; ≟-off-diag
+  using (¬Fin0; _≟_; ≟-≡-refl; ≟-≢
         ; cast-involutive; opposite-involutive
         ; punchInᵢ≢i; punchOut-punchIn; punchIn-punchOut
         ; punchOut-cong; punchOut-cong′)
@@ -229,10 +229,10 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 
   inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ k with i ≟ k
-  ... | yes i≡k rewrite ≟-diag-refl j = i≡k
+  ... | yes i≡k rewrite ≟-≡-refl j = i≡k
   ... | no  i≢k
     with j≢punchInⱼπʳpunchOuti≢k ← punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym
-    rewrite ≟-off-diag j≢punchInⱼπʳpunchOuti≢k
+    rewrite ≟-≢ j≢punchInⱼπʳpunchOuti≢k
     = begin
     punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩
     punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩
@@ -242,10 +242,10 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ k with j ≟ k
-  ... | yes j≡k rewrite ≟-diag-refl i = j≡k
+  ... | yes j≡k rewrite ≟-≡-refl i = j≡k
   ... | no  j≢k
     with i≢punchInᵢπˡpunchOutj≢k ← punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym
-    rewrite ≟-off-diag i≢punchInᵢπˡpunchOutj≢k
+    rewrite ≟-≢ i≢punchInᵢπˡpunchOutj≢k
     = begin
     punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
     punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
@@ -340,7 +340,7 @@ insert-remove {m = m} {n = n} i π j with i ≟ j
   π ⟨$⟩ʳ j                           ∎
 
 remove-insert : ∀ i j (π : Permutation m n) → remove i (insert i j π) ≈ π
-remove-insert i j π k rewrite ≟-diag-refl i = begin
+remove-insert i j π k rewrite ≟-≡-refl i = begin
   punchOut {i = j} _                               ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩
   punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym) ≡⟨ punchOut-punchIn j ⟩
   π ⟨$⟩ʳ k                                         ∎
diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda
index f126906600..b8597674f8 100644
--- a/src/Data/Fin/Permutation/Components.agda
+++ b/src/Data/Fin/Permutation/Components.agda
@@ -11,7 +11,7 @@ module Data.Fin.Permutation.Components where
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Fin.Base using (Fin; suc; opposite; toℕ)
 open import Data.Fin.Properties
-  using (_≟_; ≟-diag; ≟-diag-refl
+  using (_≟_; ≟-≡; ≟-≡-refl
         ; opposite-prop; opposite-involutive; opposite-suc)
 open import Relation.Nullary.Decidable.Core using (does; yes; no)
 open import Relation.Binary.PropositionalEquality.Core
@@ -42,15 +42,15 @@ transpose[i,i,j]≡j i j with j ≟ i in j≟i
 transpose[i,j,j]≡i : ∀ {n} (i j : Fin n) → transpose i j j ≡ i
 transpose[i,j,j]≡i i j with j ≟ i
 ... | yes j≡i                     = j≡i
-... | no  _ rewrite ≟-diag-refl j = refl
+... | no  _ rewrite ≟-≡-refl j = refl
 
 transpose[i,j,i]≡j : ∀ {n} (i j : Fin n) → transpose i j i ≡ j
-transpose[i,j,i]≡j i j rewrite ≟-diag-refl i = refl
+transpose[i,j,i]≡j i j rewrite ≟-≡-refl i = refl
 
 transpose-transpose : ∀ {n} {i j k l : Fin n} →
                       transpose i j k ≡ l → transpose j i l ≡ k
 transpose-transpose {n} {i} {j} {k} {l} eq with k ≟ i in k≟i
-... | yes k≡i rewrite ≟-diag (sym eq) = sym k≡i
+... | yes k≡i rewrite ≟-≡ (sym eq) = sym k≡i
 ... | no k≢i with k ≟ j in k≟j
 ...   | yes k≡j rewrite eq | transpose[i,j,j]≡i j l = sym k≡j
 ...   | no  k≢j rewrite eq | k≟j | k≟i = refl

From a8dfef9087e714b12628c629669d695dcaedfe32 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 3 Jul 2025 08:13:52 +0100
Subject: [PATCH 21/21] restore: original alignment

---
 src/Data/Fin/Permutation.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 5606d3773b..078e53c3bb 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -335,9 +335,9 @@ insert-remove : ∀ i (π : Permutation (suc m) (suc n)) → insert i (π ⟨$
 insert-remove {m = m} {n = n} i π j with i ≟ j
 ... | yes i≡j = cong (π ⟨$⟩ʳ_) i≡j
 ... | no  i≢j = begin
-  punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π)))                             ≡⟨ punchIn-punchOut _ ⟩
-  π ⟨$⟩ʳ punchIn i (punchOut i≢j)    ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩
-  π ⟨$⟩ʳ j                           ∎
+  punchIn (π ⟨$⟩ʳ i) (punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π))) ≡⟨ punchIn-punchOut _ ⟩
+  π ⟨$⟩ʳ punchIn i (punchOut i≢j) ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩
+  π ⟨$⟩ʳ j ∎
 
 remove-insert : ∀ i j (π : Permutation m n) → remove i (insert i j π) ≈ π
 remove-insert i j π k rewrite ≟-≡-refl i = begin