From eb70ab3881e47510f8474a2408939e65d6fdc4e2 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Sun, 3 Jan 2021 23:11:27 +0000
Subject: [PATCH 1/3] Add `begin-irrefl` reasoning combinator

---
 CHANGELOG.md                                  | 19 ++++++++++++++++
 src/Data/Integer/Properties.agda              |  6 ++++-
 .../List/Relation/Unary/Any/Properties.agda   |  1 -
 src/Data/Nat/Binary/Properties.agda           | 22 +++++++++++++------
 src/Data/Nat/Properties.agda                  |  6 ++++-
 src/Data/Rational/Properties.agda             |  6 ++++-
 .../Rational/Unnormalised/Properties.agda     |  5 +++++
 .../Relation/Unary/Any/Properties.agda        | 13 +++++------
 .../Vec/Relation/Binary/Lex/NonStrict.agda    |  5 +++++
 src/Data/Vec/Relation/Binary/Lex/Strict.agda  |  6 +++++
 .../Binary/Reasoning/Base/Triple.agda         | 15 ++++++++++++-
 .../Binary/Reasoning/PartialOrder.agda        | 11 +++++++---
 .../Binary/Reasoning/StrictPartialOrder.agda  |  5 +++++
 13 files changed, 98 insertions(+), 22 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2220cd38fd..21f03b669f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -74,6 +74,8 @@ Non-backwards compatible changes
   only a breaking change if you were supplying the module arguments upon import, in which
   case you will have to change to supplying them upon application of the proofs.
 
+* In `Relation.Binary.Reasoning.Base.Triple`, added a new parameter `<-irrefl : Irreflexive _≈_ _<_`
+
 Deprecated modules
 ------------------
 
@@ -1085,3 +1087,20 @@ Other minor additions
   ```agda
   contradiction₂ : P ⊎ Q → ¬ P → ¬ Q → Whatever
   ```
+
+* In `Relation.Binary.Reasoning.Base.Triple` new function:
+  ```agda
+  begin-irrefl : Irreflexive _≈_ _<_ → (r : x IsRelatedTo x) → {s : True (IsStrict? r)} → A
+  ```
+  Specialised versions are available in:
+  ```
+  Data.Nat.Properties
+  Data.Nat.Binary.Properties
+  Data.Integer.Properties
+  Data.Rational.Unnormalised.Properties
+  Data.Rational.Properties
+  Data.Vec.Relation.Binary.Lex.Strict
+  Data.Vec.Relation.Binary.Lex.NonStrict
+  Relation.Binary.Reasoning.StrictPartialOrder
+  Relation.Binary.Reasoning.PartialOrder
+  ```
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 2ccf50a412..d5a8a95878 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -362,8 +362,12 @@ module ≤-Reasoning where
     <⇒≤
     <-≤-trans
     ≤-<-trans
+    as Reasoning
     public
-    hiding (step-≈; step-≈˘)
+    hiding (begin-irrefl; step-≈; step-≈˘)
+
+  infix 1 begin-irrefl_
+  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
 
 ------------------------------------------------------------------------
 -- Properties of Positive/NonPositive/Negative/NonNegative and _≤_/_<_
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index 29f42dbeba..f807b54715 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -255,7 +255,6 @@ Any-×⁻ pq with Prod.map₂ (Prod.map₂ find) (find pq)
 
     (p , q) ∎
 
-
   to∘from : ∀ pq → Any-×⁺ {xs = xs} (Any-×⁻ pq) ≡ pq
   to∘from pq
     with find pq
diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index d8479c4a7e..d330ba6366 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -27,7 +27,6 @@ open import Relation.Binary.Consequences
 open import Relation.Binary.Morphism
 import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphism
 open import Relation.Binary.PropositionalEquality
-import Relation.Binary.Reasoning.Base.Triple as InequalityReasoning
 open import Relation.Nullary using (¬_; yes; no)
 import Relation.Nullary.Decidable as Dec
 open import Relation.Nullary.Negation using (contradiction)
@@ -523,12 +522,21 @@ x ≤? y with <-cmp x y
 ------------------------------------------------------------------------------
 -- Equational reasoning for _≤_ and _<_
 
-module ≤-Reasoning = InequalityReasoning
-  ≤-isPreorder
-  <-trans
-  (resp₂ _<_) <⇒≤
-  <-≤-trans ≤-<-trans
-  hiding (step-≈; step-≈˘)
+module ≤-Reasoning where
+
+  open import Relation.Binary.Reasoning.Base.Triple
+    ≤-isPreorder
+    <-trans
+    (resp₂ _<_)
+    <⇒≤
+    <-≤-trans
+    ≤-<-trans
+    as Reasoning
+    public
+    hiding (begin-irrefl; step-≈; step-≈˘)
+
+  infix 1 begin-irrefl_
+  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
 
 ------------------------------------------------------------------------------
 -- Properties of _<ℕ_
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 490de71a37..b32c5c7f16 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -449,8 +449,12 @@ module ≤-Reasoning where
     <⇒≤
     <-transˡ
     <-transʳ
+    as Reasoning
     public
-    hiding (step-≈; step-≈˘)
+    hiding (begin-irrefl; step-≈; step-≈˘)
+
+  infix 1 begin-irrefl_
+  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
 
 open ≤-Reasoning
 
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index c6923d0f97..3c5ec682fa 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -689,8 +689,12 @@ module ≤-Reasoning where
     <⇒≤
     <-≤-trans
     ≤-<-trans
+    as Reasoning
     public
-    hiding (step-≈; step-≈˘)
+    hiding (begin-irrefl; step-≈; step-≈˘)
+
+  infix 1 begin-irrefl_
+  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
 
 ------------------------------------------------------------------------
 -- Properties of Positive/NonPositive/Negative/NonNegative and _≤_/_<_
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 155b9f6d13..f45ad5d64e 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -514,7 +514,12 @@ module ≤-Reasoning where
     <⇒≤
     <-≤-trans
     ≤-<-trans
+    as Reasoning
     public
+    hiding (begin-irrefl)
+
+  infix 1 begin-irrefl_
+  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
 
 ------------------------------------------------------------------------
 -- Properties of ↥_/↧_
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index d358ccd01b..aeb1474ff9 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -30,7 +30,6 @@ open StrictTotalOrder sto renaming (Carrier to Key); open Eq using (_≉_; sym;
 
 import Relation.Binary.Reasoning.StrictPartialOrder as <-Reasoning
 
-
 private
   variable
     v p q : Level
@@ -188,33 +187,33 @@ module _ {V : Value v} where
                                      joinʳ⁺-right⁺ kv lk ku′ bal (Any-insertWith-just ku seg′ pr rp)
 
     -- impossible cases
-    ... | here eq  | tri< k<k′ _ _ = flip contradiction (irrefl⁺ [ k ]) $ begin-strict
+    ... | here eq  | tri< k<k′ _ _ = begin-irrefl
       [ k  ] <⟨ [ k<k′ ]ᴿ ⟩
       [ k′ ] ≈⟨ [ sym eq ]ᴱ ⟩
       [ k  ] ∎
-    ... | here eq  | tri> _ _ k>k′ = flip contradiction (irrefl⁺ [ k ]) $ begin-strict
+    ... | here eq  | tri> _ _ k>k′ = begin-irrefl
       [ k  ] ≈⟨ [ eq ]ᴱ ⟩
       [ k′ ] <⟨ [ k>k′ ]ᴿ ⟩
       [ k  ] ∎
-    ... | left lp  | tri≈ _ k≈k′ _ = flip contradiction (irrefl⁺ [ k ]) $ begin-strict
+    ... | left lp  | tri≈ _ k≈k′ _ = begin-irrefl
       let k″ = Any.lookup lp .key; k≈k″ = lookup-result lp; (_ , k″<k′) = lookup-bounded lp in
       [ k  ] ≈⟨ [ k≈k″ ]ᴱ ⟩
       [ k″ ] <⟨ k″<k′ ⟩
       [ k′ ] ≈⟨ [ sym k≈k′ ]ᴱ ⟩
       [ k  ] ∎
-    ... | left lp  | tri> _ _ k>k′ = flip contradiction (irrefl⁺ [ k ]) $ begin-strict
+    ... | left lp  | tri> _ _ k>k′ = begin-irrefl
       let k″ = Any.lookup lp .key; k≈k″ = lookup-result lp; (_ , k″<k′) = lookup-bounded lp in
       [ k  ] ≈⟨ [ k≈k″ ]ᴱ ⟩
       [ k″ ] <⟨ k″<k′ ⟩
       [ k′ ] <⟨ [ k>k′ ]ᴿ ⟩
       [ k  ] ∎
-    ... | right rp | tri< k<k′ _ _ = flip contradiction (irrefl⁺ [ k ]) $ begin-strict
+    ... | right rp | tri< k<k′ _ _ = begin-irrefl
       let k″ = Any.lookup rp .key; k≈k″ = lookup-result rp; (k′<k″ , _) = lookup-bounded rp in
       [ k  ] <⟨ [ k<k′ ]ᴿ ⟩
       [ k′ ] <⟨ k′<k″ ⟩
       [ k″ ] ≈⟨ [ sym k≈k″ ]ᴱ ⟩
       [ k  ] ∎
-    ... | right rp | tri≈ _ k≈k′ _ = flip contradiction (irrefl⁺ [ k ]) $ begin-strict
+    ... | right rp | tri≈ _ k≈k′ _ = begin-irrefl
       let k″ = Any.lookup rp .key; k≈k″ = lookup-result rp; (k′<k″ , _) = lookup-bounded rp in
       [ k  ] ≈⟨ [ k≈k′ ]ᴱ ⟩
       [ k′ ] <⟨ k′<k″ ⟩
diff --git a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
index f71295ece7..62ec103a0b 100644
--- a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
@@ -261,4 +261,9 @@ module ≤-Reasoning  {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂}
     <⇒≤
     (<-transˡ ≼-po)
     (<-transʳ ≼-po)
+    as Reasoning
     public
+    hiding (begin-irrefl)
+
+  infix 1 begin-irrefl_
+  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
index 954de905b2..4ba3b9515d 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
@@ -292,6 +292,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
 
 module ≤-Reasoning {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂}
                    (≈-isEquivalence : IsEquivalence _≈_)
+                   (≺-irrefl : Irreflexive _≈_ _≺_)
                    (≺-trans : Transitive _≺_)
                    (≺-resp-≈ : _≺_ Respects₂ _≈_)
                    (n : ℕ)
@@ -307,4 +308,9 @@ module ≤-Reasoning {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂}
     (<⇒≤ {m = n})
     (<-transˡ ≈-isPartialEquivalence ≺-resp-≈ ≺-trans)
     (<-transʳ ≈-isPartialEquivalence ≺-resp-≈ ≺-trans)
+    as Reasoning
     public
+    hiding (begin-irrefl)
+
+  infix 1 begin-irrefl_
+  begin-irrefl_ = Reasoning.begin-irrefl (<-irrefl ≺-irrefl)
diff --git a/src/Relation/Binary/Reasoning/Base/Triple.agda b/src/Relation/Binary/Reasoning/Base/Triple.agda
index 32c384d24c..81a62071c2 100644
--- a/src/Relation/Binary/Reasoning/Base/Triple.agda
+++ b/src/Relation/Binary/Reasoning/Base/Triple.agda
@@ -24,8 +24,9 @@ open import Function.Base using (case_of_; id)
 open import Level using (Level; _⊔_; Lift; lift)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym)
-open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Nullary using (Dec; yes; no; ¬_)
 open import Relation.Nullary.Decidable using (True; toWitness)
+open import Relation.Nullary.Negation using (contradiction)
 
 open IsPreorder isPreorder
   renaming
@@ -93,6 +94,18 @@ begin-strict_ r {s} = extractStrict (toWitness s)
 begin-equality_ : ∀ {x y} (r : x IsRelatedTo y) → {s : True (IsEquality? r)} → x ≈ y
 begin-equality_ r {s} = extractEquality (toWitness s)
 
+
+begin-irrefl : Irreflexive _≈_ _<_ →
+                ∀ {x} (r : x IsRelatedTo x) {s : True (IsStrict? r)} →
+                ∀ {a} {A : Set a} → A
+begin-irrefl <-irrefl {x} r {s} =  contradiction x<x x≮x where
+
+  x<x : x < x
+  x<x = extractStrict (toWitness s)
+
+  x≮x : ¬ (x < x)
+  x≮x = <-irrefl Eq.refl
+
 -- Step with the strict relation
 
 step-< : ∀ (x : A) {y z} → y IsRelatedTo z → x < y → x IsRelatedTo z
diff --git a/src/Relation/Binary/Reasoning/PartialOrder.agda b/src/Relation/Binary/Reasoning/PartialOrder.agda
index f358038ffe..63344bda64 100644
--- a/src/Relation/Binary/Reasoning/PartialOrder.agda
+++ b/src/Relation/Binary/Reasoning/PartialOrder.agda
@@ -45,21 +45,26 @@ module Relation.Binary.Reasoning.PartialOrder
   {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where
 
 open Poset P
-import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as Strict
+open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_
+  as Strict
+  using (_<_)
 
 ------------------------------------------------------------------------
 -- Re-export contents of base module
 
 open import Relation.Binary.Reasoning.Base.Triple
   isPreorder
-  (Strict.trans isPartialOrder)
+  (Strict.<-trans isPartialOrder)
   (Strict.<-resp-≈ isEquivalence ≤-resp-≈)
   Strict.<⇒≤
   (Strict.<-≤-trans Eq.sym trans antisym ≤-respʳ-≈)
   (Strict.≤-<-trans trans antisym ≤-respˡ-≈)
+  as Reasoning
   public
+  hiding (begin-irrefl)
 
-
+infix 1 begin-irrefl_
+begin-irrefl_ = Reasoning.begin-irrefl Strict.irrefl
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
diff --git a/src/Relation/Binary/Reasoning/StrictPartialOrder.agda b/src/Relation/Binary/Reasoning/StrictPartialOrder.agda
index a8a540e936..34f8e14d38 100644
--- a/src/Relation/Binary/Reasoning/StrictPartialOrder.agda
+++ b/src/Relation/Binary/Reasoning/StrictPartialOrder.agda
@@ -58,4 +58,9 @@ open import Relation.Binary.Reasoning.Base.Triple
   NonStrict.<⇒≤
   (NonStrict.<-≤-trans trans <-respʳ-≈)
   (NonStrict.≤-<-trans Eq.sym trans <-respˡ-≈)
+  as Reasoning
   public
+  hiding (begin-irrefl)
+
+infix 1 begin-irrefl_
+begin-irrefl_ = Reasoning.begin-irrefl irrefl

From 55f4d52819d239677222107fbf39b0752fee3376 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Tue, 26 Sep 2023 12:08:45 +0900
Subject: [PATCH 2/3] Renamed to begin-contradiction and added irrefl to module
 parameters

---
 CHANGELOG.md                                  | 41 +++++++++++--------
 src/Data/Integer/Properties.agda              |  7 +---
 src/Data/Nat/Binary/Properties.agda           |  7 +---
 src/Data/Nat/Properties.agda                  |  7 +---
 src/Data/Rational/Properties.agda             |  6 +--
 .../Rational/Unnormalised/Properties.agda     |  6 +--
 .../Relation/Unary/Any/Properties.agda        | 12 +++---
 .../Vec/Relation/Binary/Lex/NonStrict.agda    |  6 +--
 src/Data/Vec/Relation/Binary/Lex/Strict.agda  |  6 +--
 .../Binary/Reasoning/Base/Triple.agda         | 18 ++++----
 .../Binary/Reasoning/PartialOrder.agda        |  6 +--
 .../Binary/Reasoning/StrictPartialOrder.agda  |  5 +--
 12 files changed, 51 insertions(+), 76 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d8d46a4c50..4cd3b98214 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -769,6 +769,30 @@ Non-backwards compatible changes
   IO.Instances
   ```
 
+### Changes to triple reasoning interface
+
+* The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict
+  relation is irreflexive. 
+  
+* This allows the following new proof combinator:
+  ```agda
+  begin-contradiction : (r : x IsRelatedTo x) → {s : True (IsStrict? r)} → A
+  ```
+  that takes a proof that a value is strictly less than itself and then applies the principle of explosion.
+  
+* Specialised versions of this combinator are available in the following derived modules:
+  ```
+  Data.Nat.Properties
+  Data.Nat.Binary.Properties
+  Data.Integer.Properties
+  Data.Rational.Unnormalised.Properties
+  Data.Rational.Properties
+  Data.Vec.Relation.Binary.Lex.Strict
+  Data.Vec.Relation.Binary.Lex.NonStrict
+  Relation.Binary.Reasoning.StrictPartialOrder
+  Relation.Binary.Reasoning.PartialOrder
+  ```
+
 ### Other
 
 * In accordance with changes to the flags in Agda 2.6.3, all modules that previously used
@@ -3441,20 +3465,3 @@ This is a full list of proofs that have changed form to use irrelevant instance
       c ≈⟨ c≈d ⟩
       d ∎
     ```
-
-* In `Relation.Binary.Reasoning.Base.Triple` new function:
-  ```agda
-  begin-irrefl : Irreflexive _≈_ _<_ → (r : x IsRelatedTo x) → {s : True (IsStrict? r)} → A
-  ```
-  Specialised versions are available in:
-  ```
-  Data.Nat.Properties
-  Data.Nat.Binary.Properties
-  Data.Integer.Properties
-  Data.Rational.Unnormalised.Properties
-  Data.Rational.Properties
-  Data.Vec.Relation.Binary.Lex.Strict
-  Data.Vec.Relation.Binary.Lex.NonStrict
-  Relation.Binary.Reasoning.StrictPartialOrder
-  Relation.Binary.Reasoning.PartialOrder
-  ```
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 9545d3bbfd..5760b050ec 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -365,17 +365,14 @@ i≮i = <-irrefl refl
 module ≤-Reasoning where
   open import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
+    <-irrefl
     <-trans
     (resp₂ _<_)
     <⇒≤
     <-≤-trans
     ≤-<-trans
-    as Reasoning
     public
-    hiding (begin-irrefl; step-≈; step-≈˘)
-
-  infix 1 begin-irrefl_
-  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
+    hiding (step-≈; step-≈˘)
 
 ------------------------------------------------------------------------
 -- Properties of Positive/NonPositive/Negative/NonNegative and _≤_/_<_
diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index e5b0f034fc..638482131f 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -610,17 +610,14 @@ module ≤-Reasoning where
 
   open import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
+    <-irrefl
     <-trans
     (resp₂ _<_)
     <⇒≤
     <-≤-trans
     ≤-<-trans
-    as Reasoning
     public
-    hiding (begin-irrefl; step-≈; step-≈˘)
-
-  infix 1 begin-irrefl_
-  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
+    hiding (step-≈; step-≈˘)
 
 ------------------------------------------------------------------------
 -- Properties of _<ℕ_
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 333ea5ff32..5ed9b64e43 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -495,17 +495,14 @@ m<1+n⇒m≤n (s≤s m≤n) = m≤n
 module ≤-Reasoning where
   open import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
+    <-irrefl
     <-trans
     (resp₂ _<_)
     <⇒≤
     <-transˡ
     <-transʳ
-    as Reasoning
     public
-    hiding (begin-irrefl; step-≈; step-≈˘)
-
-  infix 1 begin-irrefl_
-  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
+    hiding (step-≈; step-≈˘)
 
 open ≤-Reasoning
 
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index bbd56926c5..959573218a 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -713,6 +713,7 @@ _>?_ = flip _<?_
 module ≤-Reasoning where
   import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
+    <-irrefl
     <-trans
     (resp₂ _<_)
     <⇒≤
@@ -721,7 +722,7 @@ module ≤-Reasoning where
     as Triple
 
   open Triple public
-    hiding (begin-irrefl; step-≈; step-≈˘)
+    hiding (step-≈; step-≈˘)
 
   infixr 2 step-≃ step-≃˘
 
@@ -731,9 +732,6 @@ module ≤-Reasoning where
   syntax step-≃  x y∼z x≃y = x ≃⟨  x≃y ⟩ y∼z
   syntax step-≃˘ x y∼z y≃x = x ≃˘⟨ y≃x ⟩ y∼z
 
-  infix 1 begin-irrefl_
-  begin-irrefl_ = Triple.begin-irrefl <-irrefl
-
 ------------------------------------------------------------------------
 -- Properties of Positive/NonPositive/Negative/NonNegative and _≤_/_<_
 
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index c0310aef15..2ede5bb44c 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -542,6 +542,7 @@ _>?_ = flip _<?_
 module ≤-Reasoning where
   import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
+    <-irrefl
     <-trans
     <-resp-≃
     <⇒≤
@@ -550,10 +551,7 @@ module ≤-Reasoning where
     as Triple
 
   open Triple public
-    hiding (step-≈; step-≈˘; begin-irrefl)
-
-  infix 1 begin-irrefl
-  begin-irrefl = Triple.begin-irrefl <-irrefl
+    hiding (step-≈; step-≈˘)
 
   infixr 2 step-≃ step-≃˘
 
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index da28f41c4b..49da62b10b 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -277,33 +277,33 @@ module _ {V : Value v} where
                                      joinʳ⁺-right⁺ kv lk ku′ bal (Any-insertWith-just ku seg′ pr rp)
 
     -- impossible cases
-    ... | here eq  | tri< k<k′ _ _ = begin-irrefl
+    ... | here eq  | tri< k<k′ _ _ = begin-contradiction
       [ k  ] <⟨ [ k<k′ ]ᴿ ⟩
       [ k′ ] ≈⟨ [ sym eq ]ᴱ ⟩
       [ k  ] ∎
-    ... | here eq  | tri> _ _ k>k′ = begin-irrefl
+    ... | here eq  | tri> _ _ k>k′ = begin-contradiction
       [ k  ] ≈⟨ [ eq ]ᴱ ⟩
       [ k′ ] <⟨ [ k>k′ ]ᴿ ⟩
       [ k  ] ∎
-    ... | left lp  | tri≈ _ k≈k′ _ = begin-irrefl
+    ... | left lp  | tri≈ _ k≈k′ _ = begin-contradiction
       let k″ = Any.lookup lp .key; k≈k″ = lookup-result lp; (_ , k″<k′) = lookup-bounded lp in
       [ k  ] ≈⟨ [ k≈k″ ]ᴱ ⟩
       [ k″ ] <⟨ k″<k′ ⟩
       [ k′ ] ≈⟨ [ sym k≈k′ ]ᴱ ⟩
       [ k  ] ∎
-    ... | left lp  | tri> _ _ k>k′ = begin-irrefl
+    ... | left lp  | tri> _ _ k>k′ = begin-contradiction
       let k″ = Any.lookup lp .key; k≈k″ = lookup-result lp; (_ , k″<k′) = lookup-bounded lp in
       [ k  ] ≈⟨ [ k≈k″ ]ᴱ ⟩
       [ k″ ] <⟨ k″<k′ ⟩
       [ k′ ] <⟨ [ k>k′ ]ᴿ ⟩
       [ k  ] ∎
-    ... | right rp | tri< k<k′ _ _ = begin-irrefl
+    ... | right rp | tri< k<k′ _ _ = begin-contradiction
       let k″ = Any.lookup rp .key; k≈k″ = lookup-result rp; (k′<k″ , _) = lookup-bounded rp in
       [ k  ] <⟨ [ k<k′ ]ᴿ ⟩
       [ k′ ] <⟨ k′<k″ ⟩
       [ k″ ] ≈⟨ [ sym k≈k″ ]ᴱ ⟩
       [ k  ] ∎
-    ... | right rp | tri≈ _ k≈k′ _ = begin-irrefl
+    ... | right rp | tri≈ _ k≈k′ _ = begin-contradiction
       let k″ = Any.lookup rp .key; k≈k″ = lookup-result rp; (k′<k″ , _) = lookup-bounded rp in
       [ k  ] ≈⟨ [ k≈k′ ]ᴱ ⟩
       [ k′ ] <⟨ k′<k″ ⟩
diff --git a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
index a1a42ac3a0..ff1837b85d 100644
--- a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
@@ -261,14 +261,10 @@ module ≤-Reasoning  {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂}
 
   open import Relation.Binary.Reasoning.Base.Triple
     (≤-isPreorder ≼-po {n})
+    <-irrefl
     (<-trans ≼-po)
     (<-resp₂ isEquivalence ≤-resp-≈)
     <⇒≤
     (<-transˡ ≼-po)
     (<-transʳ ≼-po)
-    as Reasoning
     public
-    hiding (begin-irrefl)
-
-  infix 1 begin-irrefl_
-  begin-irrefl_ = Reasoning.begin-irrefl <-irrefl
diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
index d690f9fc82..8c41fdfbd4 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
@@ -337,14 +337,10 @@ module ≤-Reasoning {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂}
 
   open import Relation.Binary.Reasoning.Base.Triple
     (≤-isPreorder ≈-isEquivalence ≺-trans ≺-resp-≈)
+    (<-irrefl ≺-irrefl)
     (<-trans ≈-isPartialEquivalence ≺-resp-≈ ≺-trans)
     (<-respects₂ ≈-isPartialEquivalence ≺-resp-≈)
     (<⇒≤ {m = n})
     (<-transˡ ≈-isPartialEquivalence ≺-resp-≈ ≺-trans)
     (<-transʳ ≈-isPartialEquivalence ≺-resp-≈ ≺-trans)
-    as Reasoning
     public
-    hiding (begin-irrefl)
-
-  infix 1 begin-irrefl_
-  begin-irrefl_ = Reasoning.begin-irrefl (<-irrefl ≺-irrefl)
diff --git a/src/Relation/Binary/Reasoning/Base/Triple.agda b/src/Relation/Binary/Reasoning/Base/Triple.agda
index 86e80ab52a..75aeaaef17 100644
--- a/src/Relation/Binary/Reasoning/Base/Triple.agda
+++ b/src/Relation/Binary/Reasoning/Base/Triple.agda
@@ -18,7 +18,8 @@ open import Relation.Binary.Definitions
 module Relation.Binary.Reasoning.Base.Triple {a ℓ₁ ℓ₂ ℓ₃} {A : Set a}
   {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} {_<_ : Rel A ℓ₃}
   (isPreorder : IsPreorder _≈_ _≤_)
-  (<-trans : Transitive _<_) (<-resp-≈ : _<_ Respects₂ _≈_) (<⇒≤ : _<_ ⇒ _≤_)
+  (<-irrefl : Irreflexive _≈_ _<_) (<-trans : Transitive _<_) (<-resp-≈ : _<_ Respects₂ _≈_)
+  (<⇒≤ : _<_ ⇒ _≤_)
   (<-≤-trans : Trans _<_ _≤_ _<_) (≤-<-trans : Trans _≤_ _<_ _<_)
   where
 
@@ -81,7 +82,7 @@ extractEquality (isEquality x≈y) = x≈y
 -- See `Relation.Binary.Reasoning.Base.Partial` for the design decisions
 -- behind these combinators.
 
-infix  1 begin_ begin-strict_ begin-equality_
+infix  1 begin_ begin-strict_ begin-equality_ begin-contradiction_
 infixr 2 step-< step-≤ step-≈ step-≈˘ step-≡ step-≡˘ _≡⟨⟩_
 infix  3 _∎
 
@@ -98,18 +99,13 @@ begin-strict_ r {s} = extractStrict (toWitness s)
 begin-equality_ : ∀ {x y} (r : x IsRelatedTo y) → {s : True (IsEquality? r)} → x ≈ y
 begin-equality_ r {s} = extractEquality (toWitness s)
 
-
-begin-irrefl : Irreflexive _≈_ _<_ →
-               ∀ {x} (r : x IsRelatedTo x) {s : True (IsStrict? r)} →
-               ∀ {a} {A : Set a} → A
-begin-irrefl <-irrefl {x} r {s} =  contradiction x<x x≮x where
-
+begin-contradiction_ : ∀ {x} (r : x IsRelatedTo x) {s : True (IsStrict? r)} →
+                      ∀ {a} {A : Set a} → A
+begin-contradiction_ {x} r {s} = contradiction x<x (<-irrefl Eq.refl)
+  where
   x<x : x < x
   x<x = extractStrict (toWitness s)
 
-  x≮x : ¬ (x < x)
-  x≮x = <-irrefl Eq.refl
-
 -- Step with the strict relation
 
 step-< : ∀ (x : A) {y z} → y IsRelatedTo z → x < y → x IsRelatedTo z
diff --git a/src/Relation/Binary/Reasoning/PartialOrder.agda b/src/Relation/Binary/Reasoning/PartialOrder.agda
index 97403e5ee5..f490d49330 100644
--- a/src/Relation/Binary/Reasoning/PartialOrder.agda
+++ b/src/Relation/Binary/Reasoning/PartialOrder.agda
@@ -54,17 +54,13 @@ open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_
 
 open import Relation.Binary.Reasoning.Base.Triple
   isPreorder
+  Strict.<-irrefl
   (Strict.<-trans isPartialOrder)
   (Strict.<-resp-≈ isEquivalence ≤-resp-≈)
   Strict.<⇒≤
   (Strict.<-≤-trans Eq.sym trans antisym ≤-respʳ-≈)
   (Strict.≤-<-trans trans antisym ≤-respˡ-≈)
-  as Reasoning
   public
-  hiding (begin-irrefl)
-
-infix 1 begin-irrefl_
-begin-irrefl_ = Reasoning.begin-irrefl Strict.<-irrefl
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
diff --git a/src/Relation/Binary/Reasoning/StrictPartialOrder.agda b/src/Relation/Binary/Reasoning/StrictPartialOrder.agda
index 2bf8614916..71511d5192 100644
--- a/src/Relation/Binary/Reasoning/StrictPartialOrder.agda
+++ b/src/Relation/Binary/Reasoning/StrictPartialOrder.agda
@@ -53,14 +53,11 @@ import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ as NonStrict
 
 open import Relation.Binary.Reasoning.Base.Triple
   (NonStrict.isPreorder₂ isStrictPartialOrder)
+  irrefl
   trans
   <-resp-≈
   NonStrict.<⇒≤
   (NonStrict.<-≤-trans trans <-respʳ-≈)
   (NonStrict.≤-<-trans Eq.sym trans <-respˡ-≈)
-  as Reasoning
   public
-  hiding (begin-irrefl)
 
-infix 1 begin-irrefl_
-begin-irrefl_ = Reasoning.begin-irrefl irrefl

From 4a09f57fdb7bd0e1c5a2e80860cb5dcb81e551f4 Mon Sep 17 00:00:00 2001
From: MatthewDaggitt <matthewdaggitt@gmail.com>
Date: Tue, 26 Sep 2023 12:11:21 +0900
Subject: [PATCH 3/3] Removed deprecation that snuck in

---
 src/Relation/Binary/Reasoning/PartialOrder.agda | 16 ----------------
 1 file changed, 16 deletions(-)

diff --git a/src/Relation/Binary/Reasoning/PartialOrder.agda b/src/Relation/Binary/Reasoning/PartialOrder.agda
index f490d49330..a6cb213e1a 100644
--- a/src/Relation/Binary/Reasoning/PartialOrder.agda
+++ b/src/Relation/Binary/Reasoning/PartialOrder.agda
@@ -61,19 +61,3 @@ open import Relation.Binary.Reasoning.Base.Triple
   (Strict.<-≤-trans Eq.sym trans antisym ≤-respʳ-≈)
   (Strict.≤-<-trans trans antisym ≤-respˡ-≈)
   public
-
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
--- Version 1.0
-
-infixr 2 _≈⟨⟩_
-
-_≈⟨⟩_ = _≡⟨⟩_
-{-# WARNING_ON_USAGE _≈⟨⟩_
-"Warning: _≈⟨⟩_ was deprecated in v1.0.
-Please use _≡⟨⟩_ instead."
-#-}