From a59ac04bb358fa718ad56a09c42d13b323e35383 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 26 Jul 2025 14:27:03 +0100
Subject: [PATCH 01/16] refactor: weaken type of `contradiction-irr`

---
 CHANGELOG.md                            | 4 ++++
 src/Relation/Nullary/Negation/Core.agda | 4 ++--
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3cf9a9ac90..e4cb912f3d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -15,6 +15,10 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* The type of `Relation.Nullary.Negation.Core.contradiction-irr` has been further
+  weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
+  safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.
+
 Deprecated modules
 ------------------
 
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 73876e876c..b1e9425bf2 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -47,11 +47,11 @@ _¬-⊎_ = [_,_]
 ------------------------------------------------------------------------
 -- Uses of negation
 
-contradiction-irr : .A → ¬ A → Whatever
+contradiction-irr : .A → .(¬ A) → Whatever
 contradiction-irr a ¬a = ⊥-elim-irr (¬a a)
 
 contradiction : A → ¬ A → Whatever
-contradiction a = contradiction-irr a
+contradiction a ¬a = contradiction-irr a ¬a
 
 contradiction₂ : A ⊎ B → ¬ A → ¬ B → Whatever
 contradiction₂ (inj₁ a) ¬a ¬b = contradiction a ¬a

From c57794a5d3b71ce9bd450e98eebdfdc4b0221a58 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 27 Jul 2025 08:49:44 +0100
Subject: [PATCH 02/16] refactor: make `punchOut` take an irrelevant inequality

---
 src/Data/Fin/Base.agda        |  6 +++---
 src/Data/Fin/Permutation.agda | 20 +++++++++---------
 src/Data/Fin/Properties.agda  | 39 ++++++++++++++++++++---------------
 3 files changed, 35 insertions(+), 30 deletions(-)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index c502512448..3486440c6a 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -19,7 +19,7 @@ open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
-open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction-irr)
 
 private
   variable
@@ -252,8 +252,8 @@ opposite {suc n} (suc i) = inject₁ (opposite i)
 -- This is a variant of the thick function from Conor
 -- McBride's "First-order unification by structural recursion".
 
-punchOut : ∀ {i j : Fin (suc n)} → i ≢ j → Fin n
-punchOut {_}     {zero}   {zero}  i≢j = contradiction refl i≢j
+punchOut : ∀ {i j : Fin (suc n)} → .(i ≢ j) → Fin n
+punchOut {_}     {zero}   {zero}  i≢j = contradiction-irr refl i≢j
 punchOut {_}     {zero}   {suc j} _   = j
 punchOut {suc _} {suc i}  {zero}  _   = zero
 punchOut {suc _} {suc i}  {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc))
diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 1701aa656c..5c752dc6e5 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 (punchInᵢ≢i; punchOut-punchIn;
-  punchOut-cong; punchOut-cong′; punchIn-punchOut
+  punchOut-cong; punchOut-cong′; punchOut-cong″; punchIn-punchOut
   ; _≟_; ¬Fin0; cast-involutive; opposite-involutive)
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero; 2+)
@@ -168,16 +168,16 @@ 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) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong″ i {!!} {!!} (cong πˡ (punchIn-punchOut to-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 (punchOut from-punchOut))}  _  ≡⟨ punchOut-cong″ (πʳ i) {!!} {!!} (cong πʳ (punchIn-punchOut from-punchOut)) ⟩
+    punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _  ≡⟨ punchOut-cong″ (πʳ i) {!!} {!!} (inverseʳ π) ⟩
     punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _  ≡⟨ punchOut-punchIn (πʳ i) ⟩
     j                                                                 ∎
 
@@ -233,11 +233,11 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     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
     = begin
-    punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-cong j refl) ⟩
+    punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨⟩
     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 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
@@ -246,7 +246,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     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
     = begin
-    punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-cong i refl) ⟩
+    punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨⟩
     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 ⟩
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 0f87eef534..2aaca2fbca 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -46,7 +46,8 @@ open import Relation.Binary.PropositionalEquality.Properties as ≡
   using (module ≡-Reasoning)
 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.Negation.Core
+  using (¬_; contradiction; contradiction-irr)
 open import Relation.Nullary.Reflects using (Reflects; invert)
 open import Relation.Unary as U
   using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
@@ -877,13 +878,17 @@ punchInᵢ≢i (suc i) (suc j) = punchInᵢ≢i i j ∘ suc-injective
 -- can be changed out arbitrarily (reflecting the proof-irrelevance of
 -- that argument).
 
+punchOut-cong″ : ∀ (i : Fin (suc n)) {j k} (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                j ≡ k → punchOut i≢j ≡ punchOut i≢k
+punchOut-cong″ i i≢j i≢k refl = refl
+
 punchOut-cong : ∀ (i : Fin (suc n)) {j k} {i≢j : i ≢ j} {i≢k : i ≢ k} →
                 j ≡ k → punchOut i≢j ≡ punchOut i≢k
-punchOut-cong {_}     zero    {zero}         {i≢j = 0≢0} = contradiction refl 0≢0
-punchOut-cong {_}     zero    {suc j} {zero} {i≢k = 0≢0} = contradiction refl 0≢0
+punchOut-cong {_}     zero    {zero}         {i≢j = 0≢0} = contradiction-irr refl 0≢0
+punchOut-cong {_}     zero    {suc j} {zero} {i≢k = 0≢0} = contradiction-irr refl 0≢0
 punchOut-cong {_}     zero    {suc j} {suc k}            = suc-injective
-punchOut-cong {suc n} (suc i) {zero}  {zero}   _ = refl
-punchOut-cong {suc n} (suc i) {suc j} {suc k}    = cong suc ∘ punchOut-cong i ∘ suc-injective
+punchOut-cong {suc n} (suc i) {zero}  {zero}           _ = refl
+punchOut-cong {suc n} (suc i) {suc j} {suc k} {i≢j} {i≢k} j≡k   = cong suc (punchOut-cong i {i≢j = i≢j ∘ cong suc} {i≢k = i≢k ∘ cong suc} (suc-injective j≡k))
 
 -- An alternative to 'punchOut-cong' in the which the new inequality
 -- argument is specific. Useful for enabling the omission of that
@@ -891,13 +896,14 @@ punchOut-cong {suc n} (suc i) {suc j} {suc k}    = cong suc ∘ punchOut-cong i
 
 punchOut-cong′ : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) →
                  punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym)
-punchOut-cong′ i q = punchOut-cong i q
+punchOut-cong′ i {p = p} q =
+  punchOut-cong i {i≢j = p} {i≢k = p ∘ sym ∘ trans q ∘ sym} q
 
 punchOut-injective : ∀ {i j k : Fin (suc n)}
                      (i≢j : i ≢ j) (i≢k : i ≢ k) →
                      punchOut i≢j ≡ punchOut i≢k → j ≡ k
-punchOut-injective {_}     {zero}   {zero}  {_}     0≢0 _   _     = contradiction refl 0≢0
-punchOut-injective {_}     {zero}   {_}     {zero}  _   0≢0 _     = contradiction refl 0≢0
+punchOut-injective {_}     {zero}   {zero}  {_}     0≢0 _   _     = contradiction-irr refl 0≢0
+punchOut-injective {_}     {zero}   {_}     {zero}  _   0≢0 _     = contradiction-irr refl 0≢0
 punchOut-injective {_}     {zero}   {suc j} {suc k} _   _   pⱼ≡pₖ = cong suc pⱼ≡pₖ
 punchOut-injective {suc n} {suc i}  {zero}  {zero}  _   _    _    = refl
 punchOut-injective {suc n} {suc i}  {suc j} {suc k} i≢j i≢k pⱼ≡pₖ =
@@ -905,7 +911,7 @@ punchOut-injective {suc n} {suc i}  {suc j} {suc k} i≢j i≢k pⱼ≡pₖ =
 
 punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) →
                    punchIn i (punchOut i≢j) ≡ j
-punchIn-punchOut {_}     {zero}   {zero}  0≢0 = contradiction refl 0≢0
+punchIn-punchOut {_}     {zero}   {zero}  0≢0 = contradiction-irr refl 0≢0
 punchIn-punchOut {_}     {zero}   {suc j} _   = refl
 punchIn-punchOut {suc m} {suc i}  {zero}  i≢j = refl
 punchIn-punchOut {suc m} {suc i}  {suc j} i≢j =
@@ -914,11 +920,7 @@ punchIn-punchOut {suc m} {suc i}  {suc j} i≢j =
 punchOut-punchIn : ∀ i {j : Fin n} → punchOut {i = i} {j = punchIn i j} (punchInᵢ≢i i j ∘ sym) ≡ j
 punchOut-punchIn zero    {j}     = refl
 punchOut-punchIn (suc i) {zero}  = refl
-punchOut-punchIn (suc i) {suc j} = cong suc (begin
-  punchOut (punchInᵢ≢i i j ∘ suc-injective ∘ sym ∘ cong suc)  ≡⟨ punchOut-cong i refl ⟩
-  punchOut (punchInᵢ≢i i j ∘ sym)                             ≡⟨ punchOut-punchIn i ⟩
-  j                                                           ∎)
-  where open ≡-Reasoning
+punchOut-punchIn (suc i) {suc j} = cong suc (punchOut-punchIn i)
 
 
 ------------------------------------------------------------------------
@@ -1035,9 +1037,12 @@ pigeonhole : m ℕ.< n → (f : Fin n → Fin m) → ∃₂ λ i j → i < j ×
 pigeonhole z<s               f = contradiction (f zero) λ()
 pigeonhole (s<s m<n@(s≤s _)) f with any? (λ k → f zero ≟ f (suc k))
 ... | yes (j , f₀≡fⱼ) = zero , suc j , z<s , f₀≡fⱼ
-... | no  f₀≢fₖ
-  with i , j , i<j , fᵢ≡fⱼ ← pigeonhole m<n (λ j → punchOut (f₀≢fₖ ∘ (j ,_ )))
-  = suc i , suc j , s<s i<j , punchOut-injective (f₀≢fₖ ∘ (i ,_)) _ fᵢ≡fⱼ
+... | no  ¬∃[k]f₀≡fₛₖ = 
+  let i , j , i<j , fᵢ≡fⱼ = pigeonhole m<n (λ k → punchOut (f₀≢fₛ k))
+  in suc i , suc j , s<s i<j , punchOut-injective (f₀≢fₛ i) (f₀≢fₛ j) fᵢ≡fⱼ
+  where
+  f₀≢fₛ : ∀ k → f zero ≢ f (suc k)
+  f₀≢fₛ k = ¬∃[k]f₀≡fₛₖ ∘ (k ,_)
 
 injective⇒≤ : ∀ {f : Fin m → Fin n} → Injective _≡_ _≡_ f → m ℕ.≤ n
 injective⇒≤ {zero}  {_}     {f} _   = z≤n

From 567b5e32401f9f2410a8c5d6eb6aef2a258d95d7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 28 Jul 2025 00:08:44 +0100
Subject: [PATCH 03/16] incremental progress

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

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 5c752dc6e5..7f990ed0ec 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -168,16 +168,20 @@ 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 to-punchOut)) ⟩
-    punchOut {i = i} {πˡ (πʳ (punchIn i j))}                      _  ≡⟨ punchOut-cong″ i {!!} {!!} (inverseˡ π) ⟩
+    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _
+      ≡⟨ punchOut-cong″ i from-punchOut {!!} (cong πˡ (punchIn-punchOut to-punchOut)) ⟩
+    punchOut {i = i} {πˡ (πʳ (punchIn i j))}                      _
+      ≡⟨ punchOut-cong″ i {!!} (punchInᵢ≢i i j ∘ sym) (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 from-punchOut)) ⟩
-    punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _  ≡⟨ punchOut-cong″ (πʳ i) {!!} {!!} (inverseʳ π) ⟩
+    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _
+      ≡⟨ punchOut-cong″ (πʳ i) to-punchOut {!!} (cong πʳ (punchIn-punchOut from-punchOut)) ⟩
+    punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _
+      ≡⟨ punchOut-cong″ (πʳ i) {!!} {!!} (inverseʳ π) ⟩
     punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _  ≡⟨ punchOut-punchIn (πʳ i) ⟩
     j                                                                 ∎
 
@@ -326,7 +330,7 @@ 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 i≢punchInᵢk)            ≡⟨⟩
   punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i k ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
   punchIn j (π ⟨$⟩ʳ k)                               ∎
 
@@ -343,7 +347,7 @@ remove-insert i j π k with i ≟ i
 ... | no i≢i = contradiction refl i≢i
 ... | yes _ = begin
   punchOut {i = j} _
-    ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩
+    ≡⟨ punchOut-cong″ j {!!} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym) (insert-punchIn i j π k) ⟩
   punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym)
     ≡⟨ punchOut-punchIn j ⟩
   π ⟨$⟩ʳ k
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 2aaca2fbca..b81f1b2ed1 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -900,7 +900,7 @@ punchOut-cong′ i {p = p} q =
   punchOut-cong i {i≢j = p} {i≢k = p ∘ sym ∘ trans q ∘ sym} q
 
 punchOut-injective : ∀ {i j k : Fin (suc n)}
-                     (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                     .(i≢j : i ≢ j) (i≢k : i ≢ k) →
                      punchOut i≢j ≡ punchOut i≢k → j ≡ k
 punchOut-injective {_}     {zero}   {zero}  {_}     0≢0 _   _     = contradiction-irr refl 0≢0
 punchOut-injective {_}     {zero}   {_}     {zero}  _   0≢0 _     = contradiction-irr refl 0≢0
@@ -909,7 +909,7 @@ punchOut-injective {suc n} {suc i}  {zero}  {zero}  _   _    _    = refl
 punchOut-injective {suc n} {suc i}  {suc j} {suc k} i≢j i≢k pⱼ≡pₖ =
   cong suc (punchOut-injective (i≢j ∘ cong suc) (i≢k ∘ cong suc) (suc-injective pⱼ≡pₖ))
 
-punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) →
+punchIn-punchOut : ∀ {i j : Fin (suc n)} .(i≢j : i ≢ j) →
                    punchIn i (punchOut i≢j) ≡ j
 punchIn-punchOut {_}     {zero}   {zero}  0≢0 = contradiction-irr refl 0≢0
 punchIn-punchOut {_}     {zero}   {suc j} _   = refl

From 55fff3943f22189a885ed52aa10e79d677d5c97f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 28 Jul 2025 08:04:24 +0100
Subject: [PATCH 04/16] refactor: congruence properties

---
 src/Data/Fin/Properties.agda | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index b81f1b2ed1..1c519005e8 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -878,11 +878,7 @@ punchInᵢ≢i (suc i) (suc j) = punchInᵢ≢i i j ∘ suc-injective
 -- can be changed out arbitrarily (reflecting the proof-irrelevance of
 -- that argument).
 
-punchOut-cong″ : ∀ (i : Fin (suc n)) {j k} (i≢j : i ≢ j) (i≢k : i ≢ k) →
-                j ≡ k → punchOut i≢j ≡ punchOut i≢k
-punchOut-cong″ i i≢j i≢k refl = refl
-
-punchOut-cong : ∀ (i : Fin (suc n)) {j k} {i≢j : i ≢ j} {i≢k : i ≢ k} →
+punchOut-cong : ∀ (i : Fin (suc n)) {j k} .{i≢j : i ≢ j} .{i≢k : i ≢ k} →
                 j ≡ k → punchOut i≢j ≡ punchOut i≢k
 punchOut-cong {_}     zero    {zero}         {i≢j = 0≢0} = contradiction-irr refl 0≢0
 punchOut-cong {_}     zero    {suc j} {zero} {i≢k = 0≢0} = contradiction-irr refl 0≢0
@@ -900,7 +896,7 @@ punchOut-cong′ i {p = p} q =
   punchOut-cong i {i≢j = p} {i≢k = p ∘ sym ∘ trans q ∘ sym} q
 
 punchOut-injective : ∀ {i j k : Fin (suc n)}
-                     .(i≢j : i ≢ j) (i≢k : i ≢ k) →
+                     .(i≢j : i ≢ j) .(i≢k : i ≢ k) →
                      punchOut i≢j ≡ punchOut i≢k → j ≡ k
 punchOut-injective {_}     {zero}   {zero}  {_}     0≢0 _   _     = contradiction-irr refl 0≢0
 punchOut-injective {_}     {zero}   {_}     {zero}  _   0≢0 _     = contradiction-irr refl 0≢0

From 1a31625fc15d26f75b1da9f38446650ae15cffe8 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 28 Jul 2025 08:32:49 +0100
Subject: [PATCH 05/16] refactor: simplify proofs; add one lemma

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

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 7f990ed0ec..ec355a7679 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 (punchInᵢ≢i; punchOut-punchIn;
-  punchOut-cong; punchOut-cong′; punchOut-cong″; punchIn-punchOut
+  punchOut-cong; punchIn-punchOut
   ; _≟_; ¬Fin0; cast-involutive; opposite-involutive)
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero; 2+)
@@ -28,7 +28,7 @@ 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.Negation using (contradiction)
+open import Relation.Nullary.Negation using (contradiction; contradiction-irr)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂)
 open import Relation.Binary.PropositionalEquality.Properties
@@ -167,23 +167,23 @@ 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 from-punchOut {!!} (cong πˡ (punchIn-punchOut to-punchOut)) ⟩
-    punchOut {i = i} {πˡ (πʳ (punchIn i j))}                      _
-      ≡⟨ punchOut-cong″ i {!!} (punchInᵢ≢i i j ∘ sym) (inverseˡ π) ⟩
-    punchOut {i = i} {punchIn i j}                                _  ≡⟨ punchOut-punchIn i ⟩
-    j                                                                ∎
+    from (to j)                                                          ≡⟨⟩
+    punchOut {i = i} {j = πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong i (cong πˡ (punchIn-punchOut to-punchOut)) ⟩
+    punchOut {j = πˡ (πʳ (punchIn i j))} neq                             ≡⟨ punchOut-cong i (inverseˡ π) ⟩
+    punchOut {i = i} {j = punchIn i j}                            _      ≡⟨ punchOut-punchIn i ⟩
+    j                                                                    ∎
+    where
+    neq : _
+    neq eq = punchInᵢ≢i i j (sym (trans eq (inverseˡ π)))
+    
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ j = begin
-    to (from j)                                                       ≡⟨⟩
-    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _
-      ≡⟨ punchOut-cong″ (πʳ i) to-punchOut {!!} (cong πʳ (punchIn-punchOut from-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 from-punchOut)) ⟩
+    punchOut {j = πʳ (πˡ (punchIn (πʳ i) j))} (permute-≢ from-punchOut) ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
+    punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _    ≡⟨ punchOut-punchIn (πʳ i) ⟩
+    j                                                                   ∎
 
 ------------------------------------------------------------------------
 -- Lifting
@@ -289,8 +289,9 @@ module _ (π : Permutation (suc m) (suc n)) where
   lift₀-remove p 0F      = sym p
   lift₀-remove p (suc i) = punchOut-zero (πʳ (suc i)) p
     where
-    punchOut-zero : ∀ {i} (j : Fin (suc n)) {neq} → i ≡ 0F → suc (punchOut {i = i} {j} neq) ≡ j
-    punchOut-zero 0F {neq} p = contradiction p neq
+    punchOut-zero : ∀ {i} (j : Fin (suc n)) .{neq} →
+                    i ≡ 0F → suc (punchOut {i = i} {j} neq) ≡ j
+    punchOut-zero 0F {neq} eq = contradiction-irr eq neq
     punchOut-zero (suc j) refl = refl
 
 ↔⇒≡ : Permutation m n → m ≡ n
@@ -347,7 +348,7 @@ remove-insert i j π k with i ≟ i
 ... | no i≢i = contradiction refl i≢i
 ... | yes _ = begin
   punchOut {i = j} _
-    ≡⟨ punchOut-cong″ j {!!} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym) (insert-punchIn i j π k) ⟩
+    ≡⟨ punchOut-cong j (insert-punchIn i j π k) ⟩
   punchOut {i = j} (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym)
     ≡⟨ punchOut-punchIn j ⟩
   π ⟨$⟩ʳ k

From 560903165fb4d69535c51481f5b28fbb5c9a3343 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 28 Jul 2025 08:39:10 +0100
Subject: [PATCH 06/16] fix: `CHANGELOG`

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e4cb912f3d..0309984ba4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,11 @@ Minor improvements
   weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
   safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.
 
+* Similarly type of `Data.Fin.Base.punchOut` has been weakened so that the negated
+  equational hypothesis `i ≢ j` is marked as irrelevant. This simplifies some of
+  the proofs of its properties, but also requires some slightly more explicit
+  instantiation in a couple of places.
+
 Deprecated modules
 ------------------
 

From eb6a4119b90fa8c3b52d378f4ecd6854c3114bdb Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 28 Jul 2025 08:45:47 +0100
Subject: [PATCH 07/16] fix: whitespace

---
 src/Data/Fin/Permutation.agda | 2 +-
 src/Data/Fin/Properties.agda  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index ec355a7679..7820c55120 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -175,7 +175,7 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
     where
     neq : _
     neq eq = punchInᵢ≢i i j (sym (trans eq (inverseˡ π)))
-    
+
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ j = begin
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 1c519005e8..14ff0f473b 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -1033,7 +1033,7 @@ pigeonhole : m ℕ.< n → (f : Fin n → Fin m) → ∃₂ λ i j → i < j ×
 pigeonhole z<s               f = contradiction (f zero) λ()
 pigeonhole (s<s m<n@(s≤s _)) f with any? (λ k → f zero ≟ f (suc k))
 ... | yes (j , f₀≡fⱼ) = zero , suc j , z<s , f₀≡fⱼ
-... | no  ¬∃[k]f₀≡fₛₖ = 
+... | no  ¬∃[k]f₀≡fₛₖ =
   let i , j , i<j , fᵢ≡fⱼ = pigeonhole m<n (λ k → punchOut (f₀≢fₛ k))
   in suc i , suc j , s<s i<j , punchOut-injective (f₀≢fₛ i) (f₀≢fₛ j) fᵢ≡fⱼ
   where

From 0638fb39a546bda39f796a71282878ad7d843bb5 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 29 Jul 2025 06:21:52 +0100
Subject: [PATCH 08/16] fix: tighten proof

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

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 14ff0f473b..239f789228 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -892,8 +892,7 @@ punchOut-cong {suc n} (suc i) {suc j} {suc k} {i≢j} {i≢k} j≡k   = cong suc
 
 punchOut-cong′ : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) →
                  punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym)
-punchOut-cong′ i {p = p} q =
-  punchOut-cong i {i≢j = p} {i≢k = p ∘ sym ∘ trans q ∘ sym} q
+punchOut-cong′ i q = punchOut-cong i q
 
 punchOut-injective : ∀ {i j k : Fin (suc n)}
                      .(i≢j : i ≢ j) .(i≢k : i ≢ k) →

From 709fe8229fcb7f184251a7f80c5cc016edc6e876 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 29 Jul 2025 06:25:03 +0100
Subject: [PATCH 09/16] fix: tighten proofs

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

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 239f789228..a191899dc0 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -883,8 +883,8 @@ punchOut-cong : ∀ (i : Fin (suc n)) {j k} .{i≢j : i ≢ j} .{i≢k : i ≢ k
 punchOut-cong {_}     zero    {zero}         {i≢j = 0≢0} = contradiction-irr refl 0≢0
 punchOut-cong {_}     zero    {suc j} {zero} {i≢k = 0≢0} = contradiction-irr refl 0≢0
 punchOut-cong {_}     zero    {suc j} {suc k}            = suc-injective
-punchOut-cong {suc n} (suc i) {zero}  {zero}           _ = refl
-punchOut-cong {suc n} (suc i) {suc j} {suc k} {i≢j} {i≢k} j≡k   = cong suc (punchOut-cong i {i≢j = i≢j ∘ cong suc} {i≢k = i≢k ∘ cong suc} (suc-injective j≡k))
+punchOut-cong {suc n} (suc i) {zero}  {zero}             = λ _ → refl
+punchOut-cong {suc n} (suc i) {suc j} {suc k}            = cong suc ∘ punchOut-cong i ∘ suc-injective
 
 -- An alternative to 'punchOut-cong' in the which the new inequality
 -- argument is specific. Useful for enabling the omission of that

From c2fd7fa9fab43c94971280a879a1682033e898a7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 29 Jul 2025 06:40:35 +0100
Subject: [PATCH 10/16] fix: tighten proofs

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

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 7820c55120..15d1cd7258 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -167,11 +167,11 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
 
   inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ j = begin
-    from (to j)                                                          ≡⟨⟩
-    punchOut {i = i} {j = πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong i (cong πˡ (punchIn-punchOut to-punchOut)) ⟩
-    punchOut {j = πˡ (πʳ (punchIn i j))} neq                             ≡⟨ punchOut-cong i (inverseˡ π) ⟩
-    punchOut {i = i} {j = punchIn i j}                            _      ≡⟨ punchOut-punchIn i ⟩
-    j                                                                    ∎
+    from (to j)                                                         ≡⟨⟩
+    punchOut {i = i} {j = πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _ ≡⟨ punchOut-cong i (cong πˡ (punchIn-punchOut to-punchOut)) ⟩
+    punchOut {j = πˡ (πʳ (punchIn i j))} neq                            ≡⟨ punchOut-cong i (inverseˡ π) ⟩
+    punchOut {i = i} {j = punchIn i j}                                _ ≡⟨ punchOut-punchIn i ⟩
+    j                                                                   ∎
     where
     neq : _
     neq eq = punchInᵢ≢i i j (sym (trans eq (inverseˡ π)))
@@ -179,10 +179,10 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ j = begin
-    to (from j)                                                         ≡⟨⟩
-    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _    ≡⟨ punchOut-cong (πʳ i) (cong πʳ (punchIn-punchOut from-punchOut)) ⟩
-    punchOut {j = πʳ (πˡ (punchIn (πʳ i) j))} (permute-≢ from-punchOut) ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
-    punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _    ≡⟨ punchOut-punchIn (πʳ i) ⟩
+    to (from j)                          ≡⟨⟩
+    punchOut {i = πʳ i}                _ ≡⟨ punchOut-cong (πʳ i) (cong πʳ (punchIn-punchOut from-punchOut)) ⟩
+    punchOut (permute-≢ from-punchOut)   ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
+    punchOut {i = πʳ i}                _ ≡⟨ punchOut-punchIn (πʳ i) ⟩
     j                                                                   ∎
 
 ------------------------------------------------------------------------

From 2351f5bad5ba2a2519fb163271cd9998491c3141 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 29 Jul 2025 06:59:26 +0100
Subject: [PATCH 11/16] fix: *really* tighten proofs

---
 src/Data/Fin/Permutation.agda | 25 ++++++++++++++++---------
 1 file changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 15d1cd7258..78d3498759 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -167,23 +167,30 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
 
   inverseʳ′ : StrictlyInverseʳ _≡_ to from
   inverseʳ′ j = begin
-    from (to j)                                                         ≡⟨⟩
-    punchOut {i = i} {j = πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _ ≡⟨ punchOut-cong i (cong πˡ (punchIn-punchOut to-punchOut)) ⟩
-    punchOut {j = πˡ (πʳ (punchIn i j))} neq                            ≡⟨ punchOut-cong i (inverseˡ π) ⟩
-    punchOut {i = i} {j = punchIn i j}                                _ ≡⟨ punchOut-punchIn i ⟩
+    from (to j)        ≡⟨⟩
+    punchOut {i = i} _ ≡⟨ punchOut-cong i (cong πˡ eq) ⟩
+    punchOut neq       ≡⟨ punchOut-cong i (inverseˡ π) ⟩
+    punchOut {i = i} _ ≡⟨ punchOut-punchIn i ⟩
     j                                                                   ∎
     where
-    neq : _
+    eq : punchIn (πʳ i) (to j) ≡ πʳ (punchIn i j)
+    eq = punchIn-punchOut to-punchOut
+    neq : i ≢ πˡ (πʳ (punchIn i j))
     neq eq = punchInᵢ≢i i j (sym (trans eq (inverseˡ π)))
 
 
   inverseˡ′ : StrictlyInverseˡ _≡_ to from
   inverseˡ′ j = begin
-    to (from j)                          ≡⟨⟩
-    punchOut {i = πʳ i}                _ ≡⟨ punchOut-cong (πʳ i) (cong πʳ (punchIn-punchOut from-punchOut)) ⟩
-    punchOut (permute-≢ from-punchOut)   ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
-    punchOut {i = πʳ i}                _ ≡⟨ punchOut-punchIn (πʳ i) ⟩
+    to (from j)           ≡⟨⟩
+    punchOut {i = πʳ i} _ ≡⟨ punchOut-cong (πʳ i) (cong πʳ eq) ⟩
+    punchOut neq          ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
+    punchOut {i = πʳ i} _ ≡⟨ punchOut-punchIn (πʳ i) ⟩
     j                                                                   ∎
+    where
+    eq : punchIn i (from j) ≡ πˡ (punchIn (πʳ i) j)
+    eq = punchIn-punchOut from-punchOut
+    neq : πʳ i ≢ πʳ (πˡ (punchIn (πʳ i) j))
+    neq = permute-≢ from-punchOut
 
 ------------------------------------------------------------------------
 -- Lifting

From 5e2ec9d05462151175b043845606471ffaf4ec44 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 29 Jul 2025 07:19:41 +0100
Subject: [PATCH 12/16] tidy up

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

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 78d3498759..72eac0935e 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -171,7 +171,7 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
     punchOut {i = i} _ ≡⟨ punchOut-cong i (cong πˡ eq) ⟩
     punchOut neq       ≡⟨ punchOut-cong i (inverseˡ π) ⟩
     punchOut {i = i} _ ≡⟨ punchOut-punchIn i ⟩
-    j                                                                   ∎
+    j                  ∎
     where
     eq : punchIn (πʳ i) (to j) ≡ πʳ (punchIn i j)
     eq = punchIn-punchOut to-punchOut
@@ -185,7 +185,7 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
     punchOut {i = πʳ i} _ ≡⟨ punchOut-cong (πʳ i) (cong πʳ eq) ⟩
     punchOut neq          ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
     punchOut {i = πʳ i} _ ≡⟨ punchOut-punchIn (πʳ i) ⟩
-    j                                                                   ∎
+    j                     ∎
     where
     eq : punchIn i (from j) ≡ πˡ (punchIn (πʳ i) j)
     eq = punchIn-punchOut from-punchOut

From 2f5d537c7a309838bdd8ca8d3cecf17def6870be Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 29 Jul 2025 07:52:14 +0100
Subject: [PATCH 13/16] fix: improve `CHANGELOG` text

---
 CHANGELOG.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e0fe3a829d..0c15d77763 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,10 +21,10 @@ Minor improvements
   weakened so that the negated hypothesis `¬ A` is marked as irrelevant. This is
   safe to do, in view of `Relation.Nullary.Recomputable.Properties.¬-recompute`.
 
-* Similarly type of `Data.Fin.Base.punchOut` has been weakened so that the negated
-  equational hypothesis `i ≢ j` is marked as irrelevant. This simplifies some of
-  the proofs of its properties, but also requires some slightly more explicit
-  instantiation in a couple of places.
+* Similarly the type of `Data.Fin.Base.punchOut` has been weakened so that the
+  negated equational hypothesis `i ≢ j` is marked as irrelevant. This simplifies
+  some of the proofs of its properties, but also requires some slightly more
+  explicit instantiation in a couple of places.
 
 * Refactored usages of `+-∸-assoc 1` to `∸-suc` in:
   ```agda

From a4dd7f295494b7f9d51c821b321cfc016cc7f52f Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 29 Jul 2025 10:01:31 +0100
Subject: [PATCH 14/16] refactor: even more!

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

diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 72eac0935e..d822766792 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -245,7 +245,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     rewrite dec-no (j ≟ punchIn j (π ⟨$⟩ʳ punchOut i≢k)) j≢punchInⱼπʳpunchOuti≢k
     = begin
     punchIn i (π ⟨$⟩ˡ punchOut j≢punchInⱼπʳpunchOuti≢k)                    ≡⟨⟩
-    punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn i (π ⟨$⟩ˡ l)) (punchOut-punchIn j) ⟩
+    punchIn i (π ⟨$⟩ˡ punchOut (punchInᵢ≢i j (π ⟨$⟩ʳ punchOut i≢k) ∘ sym)) ≡⟨ cong (punchIn i ∘ (π ⟨$⟩ˡ_)) (punchOut-punchIn j) ⟩
     punchIn i (π ⟨$⟩ˡ (π ⟨$⟩ʳ punchOut i≢k))                               ≡⟨ cong (punchIn i) (inverseˡ π) ⟩
     punchIn i (punchOut i≢k)                                               ≡⟨ punchIn-punchOut i≢k ⟩
     k                                                                      ∎
@@ -258,7 +258,7 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
     rewrite dec-no (i ≟ punchIn i (π ⟨$⟩ˡ punchOut j≢k)) i≢punchInᵢπˡpunchOutj≢k
     = begin
     punchIn j (π ⟨$⟩ʳ punchOut i≢punchInᵢπˡpunchOutj≢k)                    ≡⟨⟩
-    punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
+    punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i (π ⟨$⟩ˡ punchOut j≢k) ∘ sym)) ≡⟨ cong (punchIn j ∘ (π ⟨$⟩ʳ_)) (punchOut-punchIn i) ⟩
     punchIn j (π ⟨$⟩ʳ (π ⟨$⟩ˡ punchOut j≢k))                               ≡⟨ cong (punchIn j) (inverseʳ π) ⟩
     punchIn j (punchOut j≢k)                                               ≡⟨ punchIn-punchOut j≢k ⟩
     k                                                                      ∎
@@ -334,19 +334,18 @@ lift₀-transpose i j (suc k) with does (k ≟ i)
 ...   | false = refl
 ...   | true = refl
 
-insert-punchIn : ∀ i j (π : Permutation m n) k → insert i j π ⟨$⟩ʳ punchIn i k ≡ punchIn j (π ⟨$⟩ʳ k)
+insert-punchIn : ∀ i j (π : Permutation m n) k →
+                 insert i j π ⟨$⟩ʳ punchIn i k ≡ punchIn j (π ⟨$⟩ʳ k)
 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)            ≡⟨⟩
-  punchIn j (π ⟨$⟩ʳ punchOut (punchInᵢ≢i i k ∘ sym)) ≡⟨ cong (λ l → punchIn j (π ⟨$⟩ʳ l)) (punchOut-punchIn i) ⟩
-  punchIn j (π ⟨$⟩ʳ k)                               ∎
+... | no  i≢punchInᵢk = cong (punchIn j ∘ (π ⟨$⟩ʳ_)) (punchOut-punchIn i)
 
-insert-remove : ∀ i (π : Permutation (suc m) (suc n)) → insert i (π ⟨$⟩ʳ i) (remove i π) ≈ π
-insert-remove {m = m} {n = n} i π j with i ≟ j
+insert-remove : ∀ i (π : Permutation (suc m) (suc n)) →
+                insert i (π ⟨$⟩ʳ i) (remove i π) ≈ π
+insert-remove 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) _            ≡⟨ punchIn-punchOut (punchInᵢ≢i i (punchOut i≢j) ∘ sym ∘ Injection.injective (↔⇒↣ π)) ⟩
   π ⟨$⟩ʳ punchIn i (punchOut i≢j) ≡⟨ cong (π ⟨$⟩ʳ_) (punchIn-punchOut i≢j) ⟩
   π ⟨$⟩ʳ j ∎
 
@@ -354,9 +353,6 @@ 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
-  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 (punchInᵢ≢i j (π ⟨$⟩ʳ k) ∘ sym) ≡⟨ punchOut-punchIn j ⟩
+  π ⟨$⟩ʳ k                                 ∎

From a89d1aafd41e00b0c9323647f7d4ab477e39b5dc Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 29 Jul 2025 10:58:13 +0100
Subject: [PATCH 15/16] =?UTF-8?q?deprecate:=20`punchOut-cong=E2=80=B2`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                 |  5 +++++
 src/Data/Fin/Properties.agda | 18 ++++++++++--------
 2 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0c15d77763..2ee9769093 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -41,6 +41,11 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Data.Fin.Properties`:
+  ```agda
+  punchOut-cong′  ↦  punchOut-cong
+  ```
+
 New modules
 -----------
 
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index a191899dc0..0f128f96be 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -886,14 +886,6 @@ punchOut-cong {_}     zero    {suc j} {suc k}            = suc-injective
 punchOut-cong {suc n} (suc i) {zero}  {zero}             = λ _ → refl
 punchOut-cong {suc n} (suc i) {suc j} {suc k}            = cong suc ∘ punchOut-cong i ∘ suc-injective
 
--- An alternative to 'punchOut-cong' in the which the new inequality
--- argument is specific. Useful for enabling the omission of that
--- argument during equational reasoning.
-
-punchOut-cong′ : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) →
-                 punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym)
-punchOut-cong′ i q = punchOut-cong i q
-
 punchOut-injective : ∀ {i j k : Fin (suc n)}
                      .(i≢j : i ≢ j) .(i≢k : i ≢ k) →
                      punchOut i≢j ≡ punchOut i≢k → j ≡ k
@@ -1233,3 +1225,13 @@ Please use <⇒<′ instead."
 "Warning: <′⇒≺ was deprecated in v2.0.
 Please use <′⇒< instead."
 #-}
+
+-- Version 2.4
+
+punchOut-cong′ : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) →
+                 punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym)
+punchOut-cong′ i q = punchOut-cong i q
+{-# WARNING_ON_USAGE punchOut-cong′
+"Warning: punchOut-cong′ was deprecated in v2.4.
+Please use punchOut-cong instead."
+#-}

From 8eb790225d6febaa38457991c5481c19525f84dd Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 4 Aug 2025 12:05:45 +0100
Subject: [PATCH 16/16] refactor: types of `removeAt` properties

---
 src/Data/Vec/Functional/Properties.agda | 7 ++++---
 src/Data/Vec/Properties.agda            | 7 ++++---
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda
index 6356f4945b..71bd1119ab 100644
--- a/src/Data/Vec/Functional/Properties.agda
+++ b/src/Data/Vec/Functional/Properties.agda
@@ -29,7 +29,8 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 open import Relation.Nullary.Decidable
   using (Dec; does; yes; no; map′; _×-dec_)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Negation
+  using (contradiction; contradiction-irr)
 
 import Data.Fin.Properties as Finₚ
 
@@ -236,9 +237,9 @@ insertAt-punchIn {n = suc n} xs (suc i) v (suc j) = insertAt-punchIn (tail xs) i
 -- removeAt
 
 removeAt-punchOut : ∀ (xs : Vector A (suc n))
-                  {i : Fin (suc n)} {j : Fin (suc n)} (i≢j : i ≢ j) →
+                  {i : Fin (suc n)} {j : Fin (suc n)} .(i≢j : i ≢ j) →
                   removeAt xs i (punchOut i≢j) ≡ xs j
-removeAt-punchOut {n = n}     xs {zero}  {zero}  i≢j = contradiction refl i≢j
+removeAt-punchOut {n = n}     xs {zero}  {zero}  i≢j = contradiction-irr refl i≢j
 removeAt-punchOut {n = suc n} xs {zero}  {suc j} i≢j = refl
 removeAt-punchOut {n = suc n} xs {suc i} {zero}  i≢j = refl
 removeAt-punchOut {n = suc n} xs {suc i} {suc j} i≢j = removeAt-punchOut (tail xs) (i≢j ∘ cong suc)
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 73459b360f..a75ecbc85b 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -37,7 +37,8 @@ open import Relation.Binary.PropositionalEquality.Properties
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary.Decidable.Core
   using (Dec; does; yes; _×-dec_; map′)
-open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Negation.Core
+  using (contradiction; contradiction-irr)
 import Data.Nat.GeneralisedArithmetic as ℕ
 
 private
@@ -1290,9 +1291,9 @@ toList-insertAt (x ∷ xs) (suc i) v = cong (_ List.∷_) (toList-insertAt xs i
 ------------------------------------------------------------------------
 -- removeAt
 
-removeAt-punchOut : ∀ (xs : Vec A (suc n)) {i} {j} (i≢j : i ≢ j) →
+removeAt-punchOut : ∀ (xs : Vec A (suc n)) {i} {j} .(i≢j : i ≢ j) →
                   lookup (removeAt xs i) (Fin.punchOut i≢j) ≡ lookup xs j
-removeAt-punchOut (x ∷ xs)     {zero}  {zero}  i≢j = contradiction refl i≢j
+removeAt-punchOut (x ∷ xs)     {zero}  {zero}  i≢j = contradiction-irr refl i≢j
 removeAt-punchOut (x ∷ xs)     {zero}  {suc j} i≢j = refl
 removeAt-punchOut (x ∷ y ∷ xs) {suc i} {zero}  i≢j = refl
 removeAt-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j =