From 12ad5a5bd80d78f77c02c6e15341ab6783035366 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Wed, 12 Mar 2025 16:17:30 -0400
Subject: [PATCH 1/3] =?UTF-8?q?[Refractor]=20contradiction=20over=20?=
 =?UTF-8?q?=E2=8A=A5-elim=20in=20=C3=97-antisymmetric=20def?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Product/Relation/Binary/Lex/NonStrict.agda |  7 ++++---
 src/Data/Product/Relation/Binary/Lex/Strict.agda    | 10 +++++-----
 2 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
index 8ae0458f30..599a7d011c 100644
--- a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
@@ -12,6 +12,9 @@
 module Data.Product.Relation.Binary.Lex.NonStrict where
 
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
+  using (Pointwise)
+import Data.Product.Relation.Binary.Lex.Strict as Strict
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel; _⇒_)
@@ -24,9 +27,7 @@ open import Relation.Binary.Definitions
         ; Irreflexive; Asymmetric; _Respects₂_; tri<; tri>; tri≈)
 open import Relation.Binary.Consequences
 import Relation.Binary.Construct.NonStrictToStrict as Conv
-open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
-  using (Pointwise)
-import Data.Product.Relation.Binary.Lex.Strict as Strict
+
 
 private
   variable
diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda
index 4d8223909d..f69eb5e456 100644
--- a/src/Data/Product/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda
@@ -15,11 +15,9 @@ open import Data.Product.Base
 open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
   using (Pointwise)
 open import Data.Sum.Base using (inj₁; inj₂; _-⊎-_; [_,_])
-open import Data.Empty using (⊥-elim)
 open import Function.Base using (flip; _on_; _$_; _∘_)
 open import Induction.WellFounded using (Acc; acc; WfRec; WellFounded; Acc-resp-flip-≈)
 open import Level using (Level)
-open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles
   using (Preorder; StrictPartialOrder; StrictTotalOrder)
@@ -31,6 +29,8 @@ open import Relation.Binary.Definitions
         ; tri<; tri>; tri≈)
 open import Relation.Binary.Consequences using (asym⇒irr)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_)
+open import Relation.Nullary.Negation using (contradiction)
 
 private
   variable
@@ -134,11 +134,11 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
     where
     antisym : Antisymmetric _≋_ _<ₗₑₓ_
     antisym (inj₁ x₁<y₁) (inj₁ y₁<x₁) =
-      ⊥-elim $ asym₁ x₁<y₁ y₁<x₁
+      contradiction y₁<x₁ (asym₁ x₁<y₁)
     antisym (inj₁ x₁<y₁) (inj₂ y≈≤x)  =
-      ⊥-elim $ irrefl₁ (sym₁ $ proj₁ y≈≤x) x₁<y₁
+      contradiction x₁<y₁ (irrefl₁ (sym₁ $ proj₁ y≈≤x))
     antisym (inj₂ x≈≤y)  (inj₁ y₁<x₁) =
-      ⊥-elim $ irrefl₁ (sym₁ $ proj₁ x≈≤y) y₁<x₁
+      contradiction y₁<x₁ (irrefl₁ (sym₁ $ proj₁ x≈≤y))
     antisym (inj₂ x≈≤y)  (inj₂ y≈≤x)  =
       proj₁ x≈≤y , antisym₂ (proj₂ x≈≤y) (proj₂ y≈≤x)
 

From 0c6138eef354da2f55d40ff812f60ad85aeba336 Mon Sep 17 00:00:00 2001
From: Jacques <149587529+jmougeot@users.noreply.github.com>
Date: Thu, 13 Mar 2025 14:19:06 -0400
Subject: [PATCH 2/3] Update src/Data/Product/Relation/Binary/Lex/Strict.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Data/Product/Relation/Binary/Lex/Strict.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda
index f69eb5e456..136db63bb1 100644
--- a/src/Data/Product/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda
@@ -29,7 +29,7 @@ open import Relation.Binary.Definitions
         ; tri<; tri>; tri≈)
 open import Relation.Binary.Consequences using (asym⇒irr)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_)
+open import Relation.Nullary.Decidable.Core using (yes; no; _⊎-dec_; _×-dec_)
 open import Relation.Nullary.Negation using (contradiction)
 
 private

From 9f0cb9bfb5d75bcf3bf0f716047ee10211c188aa Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Thu, 13 Mar 2025 16:57:27 -0400
Subject: [PATCH 3/3] Update src/Data/Product/Relation/Binary/Lex/Strict.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Data/Product/Relation/Binary/Lex/Strict.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda
index 136db63bb1..6fa2ab6711 100644
--- a/src/Data/Product/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda
@@ -30,7 +30,7 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.Consequences using (asym⇒irr)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Nullary.Decidable.Core using (yes; no; _⊎-dec_; _×-dec_)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 private
   variable