From 88b84eddaed686b982f4027727d03021e242450e Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Wed, 12 Mar 2025 15:00:45 -0400
Subject: [PATCH 1/3] =?UTF-8?q?=20[Refractor]=20contradiction=20over=20?=
=?UTF-8?q?=E2=8A=A5-elim=20in=20trans=E2=88=A7tri=E2=87=92resp=CA=B3=20&?=
=?UTF-8?q?=20trans=E2=88=A7tri=E2=87=92resp=CB=A1=20def?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/Relation/Binary/Consequences.agda | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 3cdb4db356..4b3d3927d3 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -15,7 +15,7 @@ open import Function.Base using (_∘_; _∘₂_; _$_; flip)
open import Level using (Level)
open import Relation.Binary.Core
open import Relation.Binary.Definitions
-open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
open import Relation.Nullary.Decidable.Core
using (yes; no; recompute; map′; dec⇒maybe)
open import Relation.Unary using (∁; Pred)
@@ -157,16 +157,16 @@ module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where
_<_ Respectsʳ _≈_
trans∧tri⇒respʳ sym ≈-tr <-tr tri {x} {y} {z} y≈z x<y with tri x z
... | tri< x<z _ _ = x<z
- ... | tri≈ _ x≈z _ = ⊥-elim (tri⇒irr tri (≈-tr x≈z (sym y≈z)) x<y)
- ... | tri> _ _ z<x = ⊥-elim (tri⇒irr tri (sym y≈z) (<-tr z<x x<y))
+ ... | tri≈ _ x≈z _ = contradiction x<y (tri⇒irr tri (≈-tr x≈z (sym y≈z)))
+ ... | tri> _ _ z<x = contradiction (<-tr z<x x<y) (tri⇒irr tri (sym y≈z))
trans∧tri⇒respˡ : Transitive _≈_ →
Transitive _<_ → Trichotomous _≈_ _<_ →
_<_ Respectsˡ _≈_
trans∧tri⇒respˡ ≈-tr <-tr tri {z} {_} {y} x≈y x<z with tri y z
... | tri< y<z _ _ = y<z
- ... | tri≈ _ y≈z _ = ⊥-elim (tri⇒irr tri (≈-tr x≈y y≈z) x<z)
- ... | tri> _ _ z<y = ⊥-elim (tri⇒irr tri x≈y (<-tr x<z z<y))
+ ... | tri≈ _ y≈z _ = contradiction x<z (tri⇒irr tri (≈-tr x≈y y≈z))
+ ... | tri> _ _ z<y = contradiction (<-tr x<z z<y) (tri⇒irr tri x≈y)
trans∧tri⇒resp : Symmetric _≈_ → Transitive _≈_ →
Transitive _<_ → Trichotomous _≈_ _<_ →
From 0174dacec3dc1992d76565962534c856fb032b69 Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Wed, 12 Mar 2025 15:01:39 -0400
Subject: [PATCH 2/3] =?UTF-8?q?=20[Refractor]=20contradiction=20over=20?=
=?UTF-8?q?=E2=8A=A5-elim=20in=20trans=E2=88=A7tri=E2=87=92resp=CA=B3=20&?=
=?UTF-8?q?=20trans=E2=88=A7tri=E2=87=92resp=CB=A1=20def?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/Relation/Binary/Consequences.agda | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 4b3d3927d3..424b48e451 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -158,7 +158,7 @@ module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where
trans∧tri⇒respʳ sym ≈-tr <-tr tri {x} {y} {z} y≈z x<y with tri x z
... | tri< x<z _ _ = x<z
... | tri≈ _ x≈z _ = contradiction x<y (tri⇒irr tri (≈-tr x≈z (sym y≈z)))
- ... | tri> _ _ z<x = contradiction (<-tr z<x x<y) (tri⇒irr tri (sym y≈z))
+ ... | tri> _ _ z<x = contradiction (<-tr z<x x<y) (tri⇒irr tri (sym y≈z))
trans∧tri⇒respˡ : Transitive _≈_ →
Transitive _<_ → Trichotomous _≈_ _<_ →
From ad73edd019aed919963e35137330423e4141f83a Mon Sep 17 00:00:00 2001
From: Jacques <jacques.mougeot@centrale-med.fr>
Date: Thu, 13 Mar 2025 14:34:53 -0400
Subject: [PATCH 3/3] contradiction over bot/elim
---
src/Relation/Binary/Consequences.agda | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 424b48e451..9add6af3a0 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -8,7 +8,6 @@
module Relation.Binary.Consequences where
-open import Data.Empty using (⊥-elim)
open import Data.Product.Base using (_,_)
open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′)
open import Function.Base using (_∘_; _∘₂_; _$_; flip)
@@ -121,7 +120,7 @@ module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where
irrefl (antisym x<y y<x) x<y
asym⇒antisym : Asymmetric _<_ → Antisymmetric _≈_ _<_
- asym⇒antisym asym x<y y<x = ⊥-elim (asym x<y y<x)
+ asym⇒antisym asym x<y y<x = contradiction y<x (asym x<y)
asym⇒irr : _<_ Respects₂ _≈_ → Symmetric _≈_ →
Asymmetric _<_ → Irreflexive _≈_ _<_