From 625f57d3511f59297723578c1cb2d103b7ccbea6 Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Sun, 5 Nov 2023 10:50:19 +0000
Subject: [PATCH 01/14] new stuff

---
 src/Data/Rational/Properties/Heyting.agda     | 100 ++++++++++++++++++
 src/Relation/Binary/Properties/DecSetoid.agda |  58 ++++++++++
 2 files changed, 158 insertions(+)
 create mode 100644 src/Data/Rational/Properties/Heyting.agda
 create mode 100644 src/Relation/Binary/Properties/DecSetoid.agda

diff --git a/src/Data/Rational/Properties/Heyting.agda b/src/Data/Rational/Properties/Heyting.agda
new file mode 100644
index 0000000000..343c920b84
--- /dev/null
+++ b/src/Data/Rational/Properties/Heyting.agda
@@ -0,0 +1,100 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Proof that the rationals form a HeytingField.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Rational.Properties.Heyting where
+
+open import Data.Rational using (ℚ; ≢-nonZero; 1/_)
+open import Data.Rational.Properties
+  using (≡-decSetoid; +-*-commutativeRing; *-inverseˡ; *-inverseʳ)
+open import Relation.Binary.Bundles using (DecSetoid)
+
+open import Relation.Binary.Properties.DecSetoid ≡-decSetoid
+
+open import Algebra.Apartness.Structures
+open import Algebra using (CommutativeRing; Invertible)
+
+open CommutativeRing +-*-commutativeRing hiding (_≉_)
+
+-- some useful lemmas -- reproduced elsewhere?
+private
+  x-y≈0→x≈y : (x y : ℚ) → (x - y) ≈ 0# → x ≈ y
+  x-y≈0→x≈y x y x-y≈0 =
+    begin
+      x
+    ≈⟨ inverseˡ-unique x (- y) x-y≈0 ⟩
+      - (- y)
+    ≈⟨ ⁻¹-involutive y ⟩
+      y
+    ∎
+    where
+      open import Relation.Binary.Reasoning.Setoid setoid
+      open import Algebra.Properties.Group +-group
+
+  x≈y→x-y≈0 : (x y : ℚ) → x ≈ y → (x - y) ≈ 0#
+  x≈y→x-y≈0 x y x≈y =
+    begin
+      x - y
+    ≈⟨ +-congʳ x≈y ⟩
+      y - y
+    ≈⟨ -‿inverseʳ y ⟩
+      0#
+    ∎
+    where
+      open import Relation.Binary.Reasoning.Setoid setoid
+      open import Algebra.Properties.Group +-group
+
+  x≉y→x-y≉0 : (x y : ℚ) → x ≉ y → (x - y) ≉ 0#
+  x≉y→x-y≉0 x y x≉y x-y≈0 = x≉y (x-y≈0→x≈y x y x-y≈0)
+
+  x*y≈z→x≉0 : ∀ x y z → z ≉ 0# → x * y ≈ z → x ≉ 0#
+  x*y≈z→x≉0 x y z z≉0 x*y≈z x≈0 =
+    z≉0
+    $ begin
+        z
+      ≈⟨ sym x*y≈z ⟩
+        x * y
+      ≈⟨ *-congʳ x≈0 ⟩
+        0# * y
+      ≈⟨ zeroˡ y ⟩
+        0#
+      ∎
+    where
+      open import Function using (_$_)
+      open import Relation.Binary.Reasoning.Setoid setoid
+
+
+  1≉0 : 1# ≉ 0#
+  1≉0 = λ ()
+
+isHeytingCommutativeRing : IsHeytingCommutativeRing _≈_ _≉_ _+_ _*_ -_ 0# 1#
+isHeytingCommutativeRing =
+  record
+  { isCommutativeRing = isCommutativeRing
+  ; isApartnessRelation = ≉-isApartnessRelation
+  ; #⇒invertible =
+    λ {x} {y} x≉y →
+      let nz = ≢-nonZero (x≉y→x-y≉0 x y x≉y)
+      in
+        ( 1/_ (x - y) {{nz}}
+        , *-inverseˡ (x - y) {{nz}} , *-inverseʳ (x - y) {{nz}}
+        )
+  ; invertible⇒# = invert→#
+  }
+  where
+    open import Data.Product using (_,_)
+
+    invert→# : ∀ {x y} → Invertible _≈_ 1# _*_ (x - y) → x ≉ y
+    invert→# {x} {y} (1/[x-y] , _ , [x-y]/[x-y]≈1) x≈y =
+      x*y≈z→x≉0 (x - y) 1/[x-y] 1# 1≉0 [x-y]/[x-y]≈1 (x≈y→x-y≈0 x y x≈y)
+
+isHeytingField : IsHeytingField _≈_ _≉_ _+_ _*_ -_ 0# 1#
+isHeytingField =
+  record
+  { isHeytingCommutativeRing = isHeytingCommutativeRing
+  ; tight = ≉-tight
+  }
diff --git a/src/Relation/Binary/Properties/DecSetoid.agda b/src/Relation/Binary/Properties/DecSetoid.agda
new file mode 100644
index 0000000000..8e33fd2a59
--- /dev/null
+++ b/src/Relation/Binary/Properties/DecSetoid.agda
@@ -0,0 +1,58 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Every decidable setoid induces tight apartness relation.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary using (DecSetoid)
+
+module Relation.Binary.Properties.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where
+
+open import Relation.Nullary using (¬_; yes; no)
+open import Relation.Nullary.Decidable using (decidable-stable)
+
+open import Data.Product using (_,_)
+open import Data.Sum using (inj₁; inj₂)
+
+open import Relation.Binary.Definitions
+  using (Irreflexive; Cotransitive; Tight; Symmetric)
+
+open import Relation.Binary
+  using (Rel; IsApartnessRelation; ApartnessRelation; IsDecEquivalence)
+
+open DecSetoid S using (_≈_; isDecEquivalence) renaming (Carrier to A)
+
+open IsDecEquivalence isDecEquivalence
+
+_≉_ : Rel A ℓ
+x ≉ y = ¬ x ≈ y
+
+≉-irrefl : Irreflexive {A = A} _≈_ _≉_
+≉-irrefl x≈y x≉y = x≉y x≈y
+
+≉-cotrans : Cotransitive _≉_
+≉-cotrans {x} {y} x≉y z with x ≟ z | z ≟ y
+≉-cotrans {x} {y} x≉y z | _ | no z≉y = inj₂ z≉y
+≉-cotrans {x} {y} x≉y z | no x≉z | _ = inj₁ x≉z
+≉-cotrans {x} {y} x≉y z | yes x≈z | yes z≈y with trans x≈z z≈y
+≉-cotrans {x} {y} x≉y z | yes x≈z | yes z≈y | x≈y = inj₁ λ _ → x≉y x≈y
+
+≉-sym : Symmetric _≉_
+≉-sym x≉y y≈x = x≉y (sym y≈x)
+
+≉-isApartnessRelation : IsApartnessRelation _≈_ _≉_
+≉-isApartnessRelation =
+  record
+  { irrefl = ≉-irrefl
+  ; sym = ≉-sym
+  ; cotrans = ≉-cotrans
+  }
+
+≉-apartnessRelation : ApartnessRelation c ℓ ℓ
+≉-apartnessRelation = record { isApartnessRelation = ≉-isApartnessRelation }
+
+≉-tight : Tight _≈_ _≉_
+≉-tight x y with x ≟ y
+≉-tight x y | d = decidable-stable d , ≉-irrefl

From 361e52d6dd478410b69f3f546f07d538f3844dc9 Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Sun, 5 Nov 2023 11:00:25 +0000
Subject: [PATCH 02/14] forgot to add bundles for rational instance of Heyting*

---
 src/Data/Rational/Properties/Heyting.agda | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/Data/Rational/Properties/Heyting.agda b/src/Data/Rational/Properties/Heyting.agda
index 343c920b84..fd11b5596f 100644
--- a/src/Data/Rational/Properties/Heyting.agda
+++ b/src/Data/Rational/Properties/Heyting.agda
@@ -8,6 +8,8 @@
 
 module Data.Rational.Properties.Heyting where
 
+open import Level using (0ℓ)
+
 open import Data.Rational using (ℚ; ≢-nonZero; 1/_)
 open import Data.Rational.Properties
   using (≡-decSetoid; +-*-commutativeRing; *-inverseˡ; *-inverseʳ)
@@ -15,7 +17,12 @@ open import Relation.Binary.Bundles using (DecSetoid)
 
 open import Relation.Binary.Properties.DecSetoid ≡-decSetoid
 
-open import Algebra.Apartness.Structures
+open import Algebra.Apartness
+  using
+  ( IsHeytingCommutativeRing; IsHeytingField
+  ; HeytingCommutativeRing; HeytingField
+  )
+
 open import Algebra using (CommutativeRing; Invertible)
 
 open CommutativeRing +-*-commutativeRing hiding (_≉_)
@@ -98,3 +105,10 @@ isHeytingField =
   { isHeytingCommutativeRing = isHeytingCommutativeRing
   ; tight = ≉-tight
   }
+
+heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ
+heytingCommutativeRing =
+  record { isHeytingCommutativeRing = isHeytingCommutativeRing }
+
+heytingField : HeytingField 0ℓ 0ℓ 0ℓ
+heytingField = record { isHeytingField = isHeytingField }

From b245af32eff2e757de2adc33729d2324bf9d83ed Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Sun, 5 Nov 2023 11:08:31 +0000
Subject: [PATCH 03/14] one more (obvious) simplification

---
 src/Relation/Binary/Properties/DecSetoid.agda | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Relation/Binary/Properties/DecSetoid.agda b/src/Relation/Binary/Properties/DecSetoid.agda
index 8e33fd2a59..67b3916d89 100644
--- a/src/Relation/Binary/Properties/DecSetoid.agda
+++ b/src/Relation/Binary/Properties/DecSetoid.agda
@@ -54,5 +54,4 @@ x ≉ y = ¬ x ≈ y
 ≉-apartnessRelation = record { isApartnessRelation = ≉-isApartnessRelation }
 
 ≉-tight : Tight _≈_ _≉_
-≉-tight x y with x ≟ y
-≉-tight x y | d = decidable-stable d , ≉-irrefl
+≉-tight x y = decidable-stable (x ≟ y) , ≉-irrefl

From 41eb821b654e5508199d1a3f0c5847dd9da5f57b Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Sun, 5 Nov 2023 11:28:00 +0000
Subject: [PATCH 04/14] a few more simplifications

---
 src/Data/Rational/Properties/Heyting.agda     | 1 -
 src/Relation/Binary/Properties/DecSetoid.agda | 3 +--
 2 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Data/Rational/Properties/Heyting.agda b/src/Data/Rational/Properties/Heyting.agda
index fd11b5596f..c10f41998b 100644
--- a/src/Data/Rational/Properties/Heyting.agda
+++ b/src/Data/Rational/Properties/Heyting.agda
@@ -13,7 +13,6 @@ open import Level using (0ℓ)
 open import Data.Rational using (ℚ; ≢-nonZero; 1/_)
 open import Data.Rational.Properties
   using (≡-decSetoid; +-*-commutativeRing; *-inverseˡ; *-inverseʳ)
-open import Relation.Binary.Bundles using (DecSetoid)
 
 open import Relation.Binary.Properties.DecSetoid ≡-decSetoid
 
diff --git a/src/Relation/Binary/Properties/DecSetoid.agda b/src/Relation/Binary/Properties/DecSetoid.agda
index 67b3916d89..cb4876c75a 100644
--- a/src/Relation/Binary/Properties/DecSetoid.agda
+++ b/src/Relation/Binary/Properties/DecSetoid.agda
@@ -36,8 +36,7 @@ x ≉ y = ¬ x ≈ y
 ≉-cotrans {x} {y} x≉y z with x ≟ z | z ≟ y
 ≉-cotrans {x} {y} x≉y z | _ | no z≉y = inj₂ z≉y
 ≉-cotrans {x} {y} x≉y z | no x≉z | _ = inj₁ x≉z
-≉-cotrans {x} {y} x≉y z | yes x≈z | yes z≈y with trans x≈z z≈y
-≉-cotrans {x} {y} x≉y z | yes x≈z | yes z≈y | x≈y = inj₁ λ _ → x≉y x≈y
+≉-cotrans {x} {y} x≉y z | yes x≈z | yes z≈y = inj₁ λ _ → x≉y (trans x≈z z≈y) 
 
 ≉-sym : Symmetric _≉_
 ≉-sym x≉y y≈x = x≉y (sym y≈x)

From 57e851cf3b1a2a9d447040e57fdf34a70dc74a53 Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Tue, 7 Nov 2023 19:24:38 +0000
Subject: [PATCH 05/14] comments on DecSetoid properties from jamesmckinna

---
 src/Relation/Binary/Properties/DecSetoid.agda | 18 +++++-------------
 src/Relation/Binary/Properties/Setoid.agda    |  5 ++++-
 2 files changed, 9 insertions(+), 14 deletions(-)

diff --git a/src/Relation/Binary/Properties/DecSetoid.agda b/src/Relation/Binary/Properties/DecSetoid.agda
index cb4876c75a..4cf3355632 100644
--- a/src/Relation/Binary/Properties/DecSetoid.agda
+++ b/src/Relation/Binary/Properties/DecSetoid.agda
@@ -10,27 +10,22 @@ open import Relation.Binary using (DecSetoid)
 
 module Relation.Binary.Properties.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where
 
-open import Relation.Nullary using (¬_; yes; no)
+open import Relation.Nullary using (yes; no)
 open import Relation.Nullary.Decidable using (decidable-stable)
 
 open import Data.Product using (_,_)
 open import Data.Sum using (inj₁; inj₂)
 
 open import Relation.Binary.Definitions
-  using (Irreflexive; Cotransitive; Tight; Symmetric)
+  using (Cotransitive; Tight)
 
 open import Relation.Binary
-  using (Rel; IsApartnessRelation; ApartnessRelation; IsDecEquivalence)
-
-open DecSetoid S using (_≈_; isDecEquivalence) renaming (Carrier to A)
+  using (IsApartnessRelation; ApartnessRelation; IsDecEquivalence)
 
+open DecSetoid S using (_≈_; _≉_; isDecEquivalence; Carrier; setoid)
 open IsDecEquivalence isDecEquivalence
 
-_≉_ : Rel A ℓ
-x ≉ y = ¬ x ≈ y
-
-≉-irrefl : Irreflexive {A = A} _≈_ _≉_
-≉-irrefl x≈y x≉y = x≉y x≈y
+open import Relation.Binary.Properties.Setoid setoid
 
 ≉-cotrans : Cotransitive _≉_
 ≉-cotrans {x} {y} x≉y z with x ≟ z | z ≟ y
@@ -38,9 +33,6 @@ x ≉ y = ¬ x ≈ y
 ≉-cotrans {x} {y} x≉y z | no x≉z | _ = inj₁ x≉z
 ≉-cotrans {x} {y} x≉y z | yes x≈z | yes z≈y = inj₁ λ _ → x≉y (trans x≈z z≈y) 
 
-≉-sym : Symmetric _≉_
-≉-sym x≉y y≈x = x≉y (sym y≈x)
-
 ≉-isApartnessRelation : IsApartnessRelation _≈_ _≉_
 ≉-isApartnessRelation =
   record
diff --git a/src/Relation/Binary/Properties/Setoid.agda b/src/Relation/Binary/Properties/Setoid.agda
index 968256077f..3c50a99711 100644
--- a/src/Relation/Binary/Properties/Setoid.agda
+++ b/src/Relation/Binary/Properties/Setoid.agda
@@ -12,7 +12,7 @@ open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Binary.Bundles using (Setoid; Preorder; Poset)
 open import Relation.Binary.Definitions
-  using (Symmetric; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
+  using (Symmetric; _Respectsˡ_; _Respectsʳ_; _Respects₂_; Irreflexive)
 open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder)
 
 module Relation.Binary.Properties.Setoid {a ℓ} (S : Setoid a ℓ) where
@@ -77,6 +77,9 @@ preorder = record
 ≉-resp₂ : _≉_ Respects₂ _≈_
 ≉-resp₂ = ≉-respʳ , ≉-respˡ
 
+≉-irrefl : Irreflexive _≈_ _≉_
+≉-irrefl x≈y x≉y = x≉y x≈y
+
 ------------------------------------------------------------------------
 -- Other properties
 

From d9cbb382f7ae93d753b65f8f46d5603c9862af79 Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Tue, 7 Nov 2023 20:41:10 +0000
Subject: [PATCH 06/14]  not working, but partially there

---
 src/Algebra/Properties/Group.agda         |  23 ++++
 src/Data/Rational/Properties.agda         |  62 +++++++++++
 src/Data/Rational/Properties/Heyting.agda | 130 +++++++++++-----------
 3 files changed, 151 insertions(+), 64 deletions(-)

diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda
index 31f9aedf39..46f5ad1243 100644
--- a/src/Algebra/Properties/Group.agda
+++ b/src/Algebra/Properties/Group.agda
@@ -106,3 +106,26 @@ inverseʳ-unique x y eq = begin
   y       ≈⟨ sym (⁻¹-involutive y) ⟩
   y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (sym (inverseˡ-unique x y eq)) ⟩
   x ⁻¹    ∎
+
+x∙y⁻¹≈ε→x≈y : (x y : Carrier) → (x ∙ y ⁻¹) ≈ ε → x ≈ y
+x∙y⁻¹≈ε→x≈y x y x∙y⁻¹≈ε =
+  begin
+    x
+  ≈⟨ inverseˡ-unique x (y ⁻¹) x∙y⁻¹≈ε ⟩
+    (y ⁻¹) ⁻¹
+  ≈⟨ ⁻¹-involutive y ⟩
+    y
+  ∎
+
+x≈y→x∙y⁻¹≈ε : (x y : Carrier) → x ≈ y → (x ∙ y ⁻¹) ≈ ε
+x≈y→x∙y⁻¹≈ε x y x≈y =
+  begin
+    x ∙ y ⁻¹
+  ≈⟨ ∙-congʳ x≈y ⟩
+    y ∙ y ⁻¹
+  ≈⟨ inverseʳ y ⟩
+    ε
+  ∎
+
+x≉y→x∙y⁻¹≉ε : (x y : Carrier) → x ≉ y → (x ∙ y ⁻¹) ≉ ε
+x≉y→x∙y⁻¹≉ε x y x≉y x∙y⁻¹≈ε = x≉y (x∙y⁻¹≈ε→x≈y x y x∙y⁻¹≈ε)
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index f0a7d11c96..842489655b 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -21,6 +21,7 @@ import Algebra.Morphism.GroupMonomorphism  as GroupMonomorphisms
 import Algebra.Morphism.RingMonomorphism   as RingMonomorphisms
 import Algebra.Lattice.Morphism.LatticeMonomorphism as LatticeMonomorphisms
 import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties
+open import Algebra.Apartness
 open import Data.Bool.Base using (T; true; false)
 open import Data.Integer.Base as ℤ using (ℤ; +_; -[1+_]; +[1+_]; +0; 0ℤ; 1ℤ; _◃_)
 open import Data.Integer.Coprimality using (coprime-divisor)
@@ -95,6 +96,9 @@ mkℚ n₁ d₁ _ ≟ mkℚ n₂ d₂ _ = map′
 ≡-decSetoid : DecSetoid 0ℓ 0ℓ
 ≡-decSetoid = decSetoid _≟_
 
+1≢0 : 1ℚ ≢ 0ℚ
+1≢0 = λ ()
+
 ------------------------------------------------------------------------
 -- mkℚ+
 ------------------------------------------------------------------------
@@ -1238,6 +1242,63 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i
   { isCommutativeRing = +-*-isCommutativeRing
   }
 
+
+------------------------------------------------------------------------
+-- Field-like structures and bundles
+module _ where
+  open CommutativeRing +-*-commutativeRing using (+-group)
+  open import Algebra.Properties.Group +-group
+
+  isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
+  isHeytingCommutativeRing =
+    record
+    { isCommutativeRing = isCommutativeRing
+    ; isApartnessRelation = ≉-isApartnessRelation
+    ; #⇒invertible = #⇒invertible
+    ; invertible⇒# = invertible⇒#
+    }
+    where
+      x*y≈z→x≉0 : ∀ x y z → z ≉ 0# → x * y ≈ z → x ≉ 0#
+      x*y≈z→x≉0 x y z z≉0 x*y≈z x≈0 =
+        z≉0
+        $ begin
+            z
+          ≈⟨ sym x*y≈z ⟩
+            x * y
+          ≈⟨ *-congʳ x≈0 ⟩
+            0# * y
+          ≈⟨ zeroˡ y ⟩
+            0#
+          ∎
+        where
+          open import Function using (_$_)
+
+      #⇒invertible : {x y : ℚ} → x ≢ y → Invertible _≡_ 1ℚ _*_ (x - y)
+      #⇒invertible {x} {y} x≉y =
+        ( 1/_ (x - y) ⦃ nz ⦄
+        , *-inverseˡ (x - y) ⦃ nz ⦄ , *-inverseʳ (x - y) ⦃ nz ⦄
+        )
+        where nz = ≢-nonZero (x≉y→x∙y⁻¹≉ε +-group x y x≉y)
+
+      invertible⇒# : ∀ {x y} → Invertible _≡_ 1ℚ _*_ (x - y) → x ≢ y
+      invertible⇒# {x} {y} (1/[x-y] , _ , [x-y]/[x-y]≈1) x≈y =
+        x*y≈z→x≉0 +-*-commutativeRing (x - y) 1/[x-y] 1# 1≢0 [x-y]/[x-y]≈1 (x≈y→x∙y⁻¹≈ε +-group x y x≈y)
+
+  isHeytingField : IsHeytingField _≈_ _≉_ _+_ _*_ -_ 0# 1#
+  isHeytingField =
+    record
+    { isHeytingCommutativeRing = isHeytingCommutativeRing
+    ; tight = ≉-tight
+    }
+
+  heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ
+  heytingCommutativeRing =
+    record { isHeytingCommutativeRing = isHeytingCommutativeRing }
+
+  heytingField : HeytingField 0ℓ 0ℓ 0ℓ
+  heytingField = record { isHeytingField = isHeytingField }
+
+
 ------------------------------------------------------------------------
 -- Properties of _*_ and _≤_
 
@@ -1665,6 +1726,7 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl
 ∣∣p∣∣≡∣p∣ p = 0≤p⇒∣p∣≡p (0≤∣p∣ p)
 
 
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------
diff --git a/src/Data/Rational/Properties/Heyting.agda b/src/Data/Rational/Properties/Heyting.agda
index c10f41998b..aaadf64b23 100644
--- a/src/Data/Rational/Properties/Heyting.agda
+++ b/src/Data/Rational/Properties/Heyting.agda
@@ -10,9 +10,12 @@ module Data.Rational.Properties.Heyting where
 
 open import Level using (0ℓ)
 
-open import Data.Rational using (ℚ; ≢-nonZero; 1/_)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
+
+open import Data.Rational using (ℚ; ≢-nonZero; 1/_; 0ℚ; 1ℚ)
 open import Data.Rational.Properties
-  using (≡-decSetoid; +-*-commutativeRing; *-inverseˡ; *-inverseʳ)
+  using
+  ( ≡-decSetoid; +-*-commutativeRing; *-inverseˡ; *-inverseʳ; 1≢0 )
 
 open import Relation.Binary.Properties.DecSetoid ≡-decSetoid
 
@@ -22,81 +25,80 @@ open import Algebra.Apartness
   ; HeytingCommutativeRing; HeytingField
   )
 
-open import Algebra using (CommutativeRing; Invertible)
-
-open CommutativeRing +-*-commutativeRing hiding (_≉_)
+open import Algebra using (CommutativeRing; Invertible; Group)
+open import Data.Product using (_,_)
 
--- some useful lemmas -- reproduced elsewhere?
 private
-  x-y≈0→x≈y : (x y : ℚ) → (x - y) ≈ 0# → x ≈ y
-  x-y≈0→x≈y x y x-y≈0 =
-    begin
-      x
-    ≈⟨ inverseˡ-unique x (- y) x-y≈0 ⟩
-      - (- y)
-    ≈⟨ ⁻¹-involutive y ⟩
-      y
-    ∎
-    where
-      open import Relation.Binary.Reasoning.Setoid setoid
-      open import Algebra.Properties.Group +-group
-
-  x≈y→x-y≈0 : (x y : ℚ) → x ≈ y → (x - y) ≈ 0#
-  x≈y→x-y≈0 x y x≈y =
-    begin
-      x - y
-    ≈⟨ +-congʳ x≈y ⟩
-      y - y
-    ≈⟨ -‿inverseʳ y ⟩
-      0#
-    ∎
-    where
-      open import Relation.Binary.Reasoning.Setoid setoid
-      open import Algebra.Properties.Group +-group
-
-  x≉y→x-y≉0 : (x y : ℚ) → x ≉ y → (x - y) ≉ 0#
-  x≉y→x-y≉0 x y x≉y x-y≈0 = x≉y (x-y≈0→x≈y x y x-y≈0)
-
-  x*y≈z→x≉0 : ∀ x y z → z ≉ 0# → x * y ≈ z → x ≉ 0#
-  x*y≈z→x≉0 x y z z≉0 x*y≈z x≈0 =
-    z≉0
-    $ begin
-        z
-      ≈⟨ sym x*y≈z ⟩
-        x * y
-      ≈⟨ *-congʳ x≈0 ⟩
-        0# * y
-      ≈⟨ zeroˡ y ⟩
-        0#
+  module _ {c ℓ} (G : Group c ℓ) where
+    open Group G
+    open import Algebra.Properties.Group G
+    open import Relation.Binary.Reasoning.Setoid setoid
+
+    x∙y⁻¹≈ε→x≈y : (x y : Carrier) → (x ∙ y ⁻¹) ≈ ε → x ≈ y
+    x∙y⁻¹≈ε→x≈y x y x∙y⁻¹≈ε =
+      begin
+        x
+      ≈⟨ inverseˡ-unique x (y ⁻¹) x∙y⁻¹≈ε ⟩
+        (y ⁻¹) ⁻¹
+      ≈⟨ ⁻¹-involutive y ⟩
+        y
+      ∎
+
+    x≈y→x∙y⁻¹≈ε : (x y : Carrier) → x ≈ y → (x ∙ y ⁻¹) ≈ ε
+    x≈y→x∙y⁻¹≈ε x y x≈y =
+      begin
+        x ∙ y ⁻¹
+      ≈⟨ ∙-congʳ x≈y ⟩
+        y ∙ y ⁻¹
+      ≈⟨ inverseʳ y ⟩
+        ε
       ∎
-    where
-      open import Function using (_$_)
-      open import Relation.Binary.Reasoning.Setoid setoid
 
+    x≉y→x∙y⁻¹≉ε : (x y : Carrier) → x ≉ y → (x ∙ y ⁻¹) ≉ ε
+    x≉y→x∙y⁻¹≉ε x y x≉y x∙y⁻¹≈ε = x≉y (x∙y⁻¹≈ε→x≈y x y x∙y⁻¹≈ε)
 
-  1≉0 : 1# ≉ 0#
-  1≉0 = λ ()
+  module _ {c ℓ} (R : CommutativeRing c ℓ) where
+    open CommutativeRing R
+    open import Relation.Binary.Reasoning.Setoid setoid
 
-isHeytingCommutativeRing : IsHeytingCommutativeRing _≈_ _≉_ _+_ _*_ -_ 0# 1#
+    x*y≈z→x≉0 : ∀ x y z → z ≉ 0# → x * y ≈ z → x ≉ 0#
+    x*y≈z→x≉0 x y z z≉0 x*y≈z x≈0 =
+      z≉0
+      $ begin
+          z
+        ≈⟨ sym x*y≈z ⟩
+          x * y
+        ≈⟨ *-congʳ x≈0 ⟩
+          0# * y
+        ≈⟨ zeroˡ y ⟩
+          0#
+        ∎
+      where
+        open import Function using (_$_)
+
+
+open CommutativeRing +-*-commutativeRing
+
+isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
 isHeytingCommutativeRing =
   record
   { isCommutativeRing = isCommutativeRing
   ; isApartnessRelation = ≉-isApartnessRelation
-  ; #⇒invertible =
-    λ {x} {y} x≉y →
-      let nz = ≢-nonZero (x≉y→x-y≉0 x y x≉y)
-      in
-        ( 1/_ (x - y) {{nz}}
-        , *-inverseˡ (x - y) {{nz}} , *-inverseʳ (x - y) {{nz}}
-        )
-  ; invertible⇒# = invert→#
+  ; #⇒invertible = #⇒invertible
+  ; invertible⇒# = invertible⇒#
   }
   where
-    open import Data.Product using (_,_)
 
-    invert→# : ∀ {x y} → Invertible _≈_ 1# _*_ (x - y) → x ≉ y
-    invert→# {x} {y} (1/[x-y] , _ , [x-y]/[x-y]≈1) x≈y =
-      x*y≈z→x≉0 (x - y) 1/[x-y] 1# 1≉0 [x-y]/[x-y]≈1 (x≈y→x-y≈0 x y x≈y)
+    #⇒invertible : {x y : ℚ} → x ≢ y → Invertible _≡_ 1ℚ _*_ (x - y)
+    #⇒invertible {x} {y} x≉y =
+      ( 1/_ (x - y) ⦃ nz ⦄
+      , *-inverseˡ (x - y) ⦃ nz ⦄ , *-inverseʳ (x - y) ⦃ nz ⦄
+      )
+      where nz = ≢-nonZero (x≉y→x∙y⁻¹≉ε +-group x y x≉y)
+
+    invertible⇒# : ∀ {x y} → Invertible _≈_ 1# _*_ (x - y) → x ≉ y
+    invertible⇒# {x} {y} (1/[x-y] , _ , [x-y]/[x-y]≈1) x≈y =
+      x*y≈z→x≉0 +-*-commutativeRing (x - y) 1/[x-y] 1# 1≢0 [x-y]/[x-y]≈1 (x≈y→x∙y⁻¹≈ε +-group x y x≈y)
 
 isHeytingField : IsHeytingField _≈_ _≉_ _+_ _*_ -_ 0# 1#
 isHeytingField =

From 968ae5e9b1c4eda2898e793e1ce5083ac59c6eb2 Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Thu, 9 Nov 2023 19:35:03 +0000
Subject: [PATCH 07/14] woo!

---
 src/Algebra/Properties/Group.agda | 24 ++++++-----------
 src/Data/Rational/Properties.agda | 43 +++++++++++++++++++------------
 2 files changed, 35 insertions(+), 32 deletions(-)

diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda
index 46f5ad1243..4da78dd984 100644
--- a/src/Algebra/Properties/Group.agda
+++ b/src/Algebra/Properties/Group.agda
@@ -108,24 +108,16 @@ inverseʳ-unique x y eq = begin
   x ⁻¹    ∎
 
 x∙y⁻¹≈ε→x≈y : (x y : Carrier) → (x ∙ y ⁻¹) ≈ ε → x ≈ y
-x∙y⁻¹≈ε→x≈y x y x∙y⁻¹≈ε =
-  begin
-    x
-  ≈⟨ inverseˡ-unique x (y ⁻¹) x∙y⁻¹≈ε ⟩
-    (y ⁻¹) ⁻¹
-  ≈⟨ ⁻¹-involutive y ⟩
-    y
-  ∎
+x∙y⁻¹≈ε→x≈y x y x∙y⁻¹≈ε = begin
+  x         ≈⟨ inverseˡ-unique x (y ⁻¹) x∙y⁻¹≈ε ⟩
+  y ⁻¹ ⁻¹  ≈⟨ ⁻¹-involutive y ⟩
+  y         ∎
 
 x≈y→x∙y⁻¹≈ε : (x y : Carrier) → x ≈ y → (x ∙ y ⁻¹) ≈ ε
-x≈y→x∙y⁻¹≈ε x y x≈y =
-  begin
-    x ∙ y ⁻¹
-  ≈⟨ ∙-congʳ x≈y ⟩
-    y ∙ y ⁻¹
-  ≈⟨ inverseʳ y ⟩
-    ε
-  ∎
+x≈y→x∙y⁻¹≈ε x y x≈y = begin
+  x ∙ y ⁻¹ ≈⟨ ∙-congʳ x≈y ⟩
+  y ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩
+  ε        ∎
 
 x≉y→x∙y⁻¹≉ε : (x y : Carrier) → x ≉ y → (x ∙ y ⁻¹) ≉ ε
 x≉y→x∙y⁻¹≉ε x y x≉y x∙y⁻¹≈ε = x≉y (x∙y⁻¹≈ε→x≈y x y x∙y⁻¹≈ε)
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 842489655b..4a97b32025 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -1246,8 +1246,12 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i
 ------------------------------------------------------------------------
 -- Field-like structures and bundles
 module _ where
-  open CommutativeRing +-*-commutativeRing using (+-group)
+  open CommutativeRing +-*-commutativeRing
+    using (+-group; zeroˡ; *-congʳ; isCommutativeRing)
+
   open import Algebra.Properties.Group +-group
+  open import Relation.Binary.Reasoning.Setoid ≡-setoid
+  open import Relation.Binary.Properties.DecSetoid ≡-decSetoid
 
   isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
   isHeytingCommutativeRing =
@@ -1258,33 +1262,40 @@ module _ where
     ; invertible⇒# = invertible⇒#
     }
     where
-      x*y≈z→x≉0 : ∀ x y z → z ≉ 0# → x * y ≈ z → x ≉ 0#
-      x*y≈z→x≉0 x y z z≉0 x*y≈z x≈0 =
+      x*y≡z→x≢0 : ∀ x y z → z ≢ 0ℚ → x * y ≡ z → x ≢ 0ℚ
+      x*y≡z→x≢0 x y z z≉0 x*y≡z x≡0 =
         z≉0
         $ begin
             z
-          ≈⟨ sym x*y≈z ⟩
+          ≈⟨ sym x*y≡z ⟩
             x * y
-          ≈⟨ *-congʳ x≈0 ⟩
-            0# * y
+          ≈⟨ *-congʳ x≡0 ⟩
+            0ℚ * y
           ≈⟨ zeroˡ y ⟩
-            0#
+            0ℚ
           ∎
         where
           open import Function using (_$_)
 
-      #⇒invertible : {x y : ℚ} → x ≢ y → Invertible _≡_ 1ℚ _*_ (x - y)
-      #⇒invertible {x} {y} x≉y =
+      #⇒invertible : {x y : ℚ} → x ≢ y → Invertible 1ℚ _*_ (x - y)
+      #⇒invertible {x} {y} x≢y =
         ( 1/_ (x - y) ⦃ nz ⦄
         , *-inverseˡ (x - y) ⦃ nz ⦄ , *-inverseʳ (x - y) ⦃ nz ⦄
         )
-        where nz = ≢-nonZero (x≉y→x∙y⁻¹≉ε +-group x y x≉y)
-
-      invertible⇒# : ∀ {x y} → Invertible _≡_ 1ℚ _*_ (x - y) → x ≢ y
-      invertible⇒# {x} {y} (1/[x-y] , _ , [x-y]/[x-y]≈1) x≈y =
-        x*y≈z→x≉0 +-*-commutativeRing (x - y) 1/[x-y] 1# 1≢0 [x-y]/[x-y]≈1 (x≈y→x∙y⁻¹≈ε +-group x y x≈y)
-
-  isHeytingField : IsHeytingField _≈_ _≉_ _+_ _*_ -_ 0# 1#
+        where
+          nz = ≢-nonZero (x≉y→x∙y⁻¹≉ε x y x≢y)
+
+      invertible⇒# : ∀ {i j} → Invertible 1ℚ _*_ (i - j) → i ≢ j
+      invertible⇒# {i} {j} (1/[i-j] , _ , [i-j]/[i-j]≡1) i≡j =
+        x*y≡z→x≢0
+          (i - j)
+          1/[i-j]
+          1ℚ
+          1≢0
+          [i-j]/[i-j]≡1
+          (x≈y→x∙y⁻¹≈ε i j i≡j)
+
+  isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
   isHeytingField =
     record
     { isHeytingCommutativeRing = isHeytingCommutativeRing

From 7b3b12caeaa50fb0b703458d4c43b16098f9f26b Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Thu, 9 Nov 2023 20:03:07 +0000
Subject: [PATCH 08/14] fix anonymous instance

---
 src/Data/Rational/Properties.agda         |  11 ++-
 src/Data/Rational/Properties/Heyting.agda | 115 ----------------------
 2 files changed, 6 insertions(+), 120 deletions(-)
 delete mode 100644 src/Data/Rational/Properties/Heyting.agda

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 4a97b32025..a568e52be5 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -1279,11 +1279,12 @@ module _ where
 
       #⇒invertible : {x y : ℚ} → x ≢ y → Invertible 1ℚ _*_ (x - y)
       #⇒invertible {x} {y} x≢y =
-        ( 1/_ (x - y) ⦃ nz ⦄
-        , *-inverseˡ (x - y) ⦃ nz ⦄ , *-inverseʳ (x - y) ⦃ nz ⦄
-        )
-        where
-          nz = ≢-nonZero (x≉y→x∙y⁻¹≉ε x y x≢y)
+        let instance _ = ≢-nonZero (x≉y→x∙y⁻¹≉ε x y x≢y)
+        in
+          ( 1/_ (x - y)
+          , *-inverseˡ (x - y)
+          , *-inverseʳ (x - y)
+          )
 
       invertible⇒# : ∀ {i j} → Invertible 1ℚ _*_ (i - j) → i ≢ j
       invertible⇒# {i} {j} (1/[i-j] , _ , [i-j]/[i-j]≡1) i≡j =
diff --git a/src/Data/Rational/Properties/Heyting.agda b/src/Data/Rational/Properties/Heyting.agda
deleted file mode 100644
index aaadf64b23..0000000000
--- a/src/Data/Rational/Properties/Heyting.agda
+++ /dev/null
@@ -1,115 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Proof that the rationals form a HeytingField.
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-module Data.Rational.Properties.Heyting where
-
-open import Level using (0ℓ)
-
-open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
-
-open import Data.Rational using (ℚ; ≢-nonZero; 1/_; 0ℚ; 1ℚ)
-open import Data.Rational.Properties
-  using
-  ( ≡-decSetoid; +-*-commutativeRing; *-inverseˡ; *-inverseʳ; 1≢0 )
-
-open import Relation.Binary.Properties.DecSetoid ≡-decSetoid
-
-open import Algebra.Apartness
-  using
-  ( IsHeytingCommutativeRing; IsHeytingField
-  ; HeytingCommutativeRing; HeytingField
-  )
-
-open import Algebra using (CommutativeRing; Invertible; Group)
-open import Data.Product using (_,_)
-
-private
-  module _ {c ℓ} (G : Group c ℓ) where
-    open Group G
-    open import Algebra.Properties.Group G
-    open import Relation.Binary.Reasoning.Setoid setoid
-
-    x∙y⁻¹≈ε→x≈y : (x y : Carrier) → (x ∙ y ⁻¹) ≈ ε → x ≈ y
-    x∙y⁻¹≈ε→x≈y x y x∙y⁻¹≈ε =
-      begin
-        x
-      ≈⟨ inverseˡ-unique x (y ⁻¹) x∙y⁻¹≈ε ⟩
-        (y ⁻¹) ⁻¹
-      ≈⟨ ⁻¹-involutive y ⟩
-        y
-      ∎
-
-    x≈y→x∙y⁻¹≈ε : (x y : Carrier) → x ≈ y → (x ∙ y ⁻¹) ≈ ε
-    x≈y→x∙y⁻¹≈ε x y x≈y =
-      begin
-        x ∙ y ⁻¹
-      ≈⟨ ∙-congʳ x≈y ⟩
-        y ∙ y ⁻¹
-      ≈⟨ inverseʳ y ⟩
-        ε
-      ∎
-
-    x≉y→x∙y⁻¹≉ε : (x y : Carrier) → x ≉ y → (x ∙ y ⁻¹) ≉ ε
-    x≉y→x∙y⁻¹≉ε x y x≉y x∙y⁻¹≈ε = x≉y (x∙y⁻¹≈ε→x≈y x y x∙y⁻¹≈ε)
-
-  module _ {c ℓ} (R : CommutativeRing c ℓ) where
-    open CommutativeRing R
-    open import Relation.Binary.Reasoning.Setoid setoid
-
-    x*y≈z→x≉0 : ∀ x y z → z ≉ 0# → x * y ≈ z → x ≉ 0#
-    x*y≈z→x≉0 x y z z≉0 x*y≈z x≈0 =
-      z≉0
-      $ begin
-          z
-        ≈⟨ sym x*y≈z ⟩
-          x * y
-        ≈⟨ *-congʳ x≈0 ⟩
-          0# * y
-        ≈⟨ zeroˡ y ⟩
-          0#
-        ∎
-      where
-        open import Function using (_$_)
-
-
-open CommutativeRing +-*-commutativeRing
-
-isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
-isHeytingCommutativeRing =
-  record
-  { isCommutativeRing = isCommutativeRing
-  ; isApartnessRelation = ≉-isApartnessRelation
-  ; #⇒invertible = #⇒invertible
-  ; invertible⇒# = invertible⇒#
-  }
-  where
-
-    #⇒invertible : {x y : ℚ} → x ≢ y → Invertible _≡_ 1ℚ _*_ (x - y)
-    #⇒invertible {x} {y} x≉y =
-      ( 1/_ (x - y) ⦃ nz ⦄
-      , *-inverseˡ (x - y) ⦃ nz ⦄ , *-inverseʳ (x - y) ⦃ nz ⦄
-      )
-      where nz = ≢-nonZero (x≉y→x∙y⁻¹≉ε +-group x y x≉y)
-
-    invertible⇒# : ∀ {x y} → Invertible _≈_ 1# _*_ (x - y) → x ≉ y
-    invertible⇒# {x} {y} (1/[x-y] , _ , [x-y]/[x-y]≈1) x≈y =
-      x*y≈z→x≉0 +-*-commutativeRing (x - y) 1/[x-y] 1# 1≢0 [x-y]/[x-y]≈1 (x≈y→x∙y⁻¹≈ε +-group x y x≈y)
-
-isHeytingField : IsHeytingField _≈_ _≉_ _+_ _*_ -_ 0# 1#
-isHeytingField =
-  record
-  { isHeytingCommutativeRing = isHeytingCommutativeRing
-  ; tight = ≉-tight
-  }
-
-heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ
-heytingCommutativeRing =
-  record { isHeytingCommutativeRing = isHeytingCommutativeRing }
-
-heytingField : HeytingField 0ℓ 0ℓ 0ℓ
-heytingField = record { isHeytingField = isHeytingField }

From d41712e63cd443c1700e2b2ca87f2cac8c6e04b2 Mon Sep 17 00:00:00 2001
From: Chris Pollard <cspollard@gmail.com>
Date: Thu, 9 Nov 2023 20:04:45 +0000
Subject: [PATCH 09/14] fix errant whitespace

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

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index a568e52be5..a3bb5d0bc7 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -1738,7 +1738,6 @@ toℚᵘ-homo-∣-∣ (mkℚ -[1+ _ ] _ _) = *≡* refl
 ∣∣p∣∣≡∣p∣ p = 0≤p⇒∣p∣≡p (0≤∣p∣ p)
 
 
-
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

From 17efee28da3af13e3293e2d4a0d802f1872b2793 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 26 Mar 2024 07:00:47 +0000
Subject: [PATCH 10/14] `fix-whitespace`

---
 src/Relation/Binary/Properties/DecSetoid.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Relation/Binary/Properties/DecSetoid.agda b/src/Relation/Binary/Properties/DecSetoid.agda
index 4cf3355632..ee952fbe6c 100644
--- a/src/Relation/Binary/Properties/DecSetoid.agda
+++ b/src/Relation/Binary/Properties/DecSetoid.agda
@@ -31,7 +31,7 @@ open import Relation.Binary.Properties.Setoid setoid
 ≉-cotrans {x} {y} x≉y z with x ≟ z | z ≟ y
 ≉-cotrans {x} {y} x≉y z | _ | no z≉y = inj₂ z≉y
 ≉-cotrans {x} {y} x≉y z | no x≉z | _ = inj₁ x≉z
-≉-cotrans {x} {y} x≉y z | yes x≈z | yes z≈y = inj₁ λ _ → x≉y (trans x≈z z≈y) 
+≉-cotrans {x} {y} x≉y z | yes x≈z | yes z≈y = inj₁ λ _ → x≉y (trans x≈z z≈y)
 
 ≉-isApartnessRelation : IsApartnessRelation _≈_ _≉_
 ≉-isApartnessRelation =

From a39d3666559b55105c23d32bbdf07bd72a97ea03 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 16 May 2024 14:43:30 +0100
Subject: [PATCH 11/14] rectified wrt `contradiction`

---
 CHANGELOG.md                               | 1 +
 src/Relation/Binary/Properties/Setoid.agda | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2b9d357511..e04b412549 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -384,6 +384,7 @@ Additions to existing modules
 
 * Added new proofs in `Relation.Binary.Properties.Setoid`:
   ```agda
+  ≉-irrefl : Irreflexive _≈_ _≉_
   ≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_
   ≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_
   ```
diff --git a/src/Relation/Binary/Properties/Setoid.agda b/src/Relation/Binary/Properties/Setoid.agda
index b7ffe2552a..43dc7e67d0 100644
--- a/src/Relation/Binary/Properties/Setoid.agda
+++ b/src/Relation/Binary/Properties/Setoid.agda
@@ -8,7 +8,7 @@
 
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘_; id; _$_; flip)
-open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.Bundles using (Setoid; Preorder; Poset)
@@ -81,7 +81,7 @@ preorder = record
 ≉-resp₂ = ≉-respʳ , ≉-respˡ
 
 ≉-irrefl : Irreflexive _≈_ _≉_
-≉-irrefl x≈y x≉y = x≉y x≈y
+≉-irrefl x≈y x≉y = contradiction x≈y x≉y
 
 ------------------------------------------------------------------------
 -- Equality is closed under composition

From 37e8e3b6d427e1ec7f7ecdcc3734b2751b7c530d Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 16 May 2024 14:53:46 +0100
Subject: [PATCH 12/14] rectified `DecSetoid` properties

---
 CHANGELOG.md                                  |  5 ++++
 src/Relation/Binary/Properties/DecSetoid.agda | 29 ++++++++-----------
 2 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e04b412549..cf564afacc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -118,6 +118,11 @@ New modules
   Relation.Binary.Construct.Interior.Symmetric
   ```
 
+* Properties of `Setoid`s with decidable equality relation:
+  ```
+  Relation.Binary.Properties.DecSetoid
+  ```
+
 * Pointwise and equality relations over indexed containers:
   ```agda
   Data.Container.Indexed.Relation.Binary.Pointwise
diff --git a/src/Relation/Binary/Properties/DecSetoid.agda b/src/Relation/Binary/Properties/DecSetoid.agda
index ee952fbe6c..7f9b323d85 100644
--- a/src/Relation/Binary/Properties/DecSetoid.agda
+++ b/src/Relation/Binary/Properties/DecSetoid.agda
@@ -6,36 +6,31 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (DecSetoid)
+open import Relation.Binary.Bundles using (DecSetoid; ApartnessRelation)
 
 module Relation.Binary.Properties.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where
 
-open import Relation.Nullary using (yes; no)
-open import Relation.Nullary.Decidable using (decidable-stable)
-
 open import Data.Product using (_,_)
 open import Data.Sum using (inj₁; inj₂)
-
 open import Relation.Binary.Definitions
   using (Cotransitive; Tight)
+import Relation.Binary.Properties.Setoid as SetoidProperties
+open import Relation.Binary.Structures
+  using (IsApartnessRelation; IsDecEquivalence)
+open import Relation.Nullary.Decidable.Core
+  using (yes; no; decidable-stable)
 
-open import Relation.Binary
-  using (IsApartnessRelation; ApartnessRelation; IsDecEquivalence)
-
-open DecSetoid S using (_≈_; _≉_; isDecEquivalence; Carrier; setoid)
-open IsDecEquivalence isDecEquivalence
-
-open import Relation.Binary.Properties.Setoid setoid
+open DecSetoid S using (_≈_; _≉_; _≟_; setoid; trans)
+open SetoidProperties setoid
 
 ≉-cotrans : Cotransitive _≉_
 ≉-cotrans {x} {y} x≉y z with x ≟ z | z ≟ y
-≉-cotrans {x} {y} x≉y z | _ | no z≉y = inj₂ z≉y
-≉-cotrans {x} {y} x≉y z | no x≉z | _ = inj₁ x≉z
-≉-cotrans {x} {y} x≉y z | yes x≈z | yes z≈y = inj₁ λ _ → x≉y (trans x≈z z≈y)
+... | _ | no z≉y = inj₂ z≉y
+... | no x≉z | _ = inj₁ x≉z
+... | yes x≈z | yes z≈y = inj₁ λ _ → x≉y (trans x≈z z≈y)
 
 ≉-isApartnessRelation : IsApartnessRelation _≈_ _≉_
-≉-isApartnessRelation =
-  record
+≉-isApartnessRelation = record
   { irrefl = ≉-irrefl
   ; sym = ≉-sym
   ; cotrans = ≉-cotrans

From 86e550d77f8226c2d7e3f62e7f319b87cbdd3716 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 16 May 2024 16:03:25 +0100
Subject: [PATCH 13/14] rectified `Group` properties

---
 CHANGELOG.md                      | 16 +++++++
 src/Algebra/Properties/Group.agda | 13 ++----
 src/Data/Rational/Properties.agda | 76 ++++++++++++-------------------
 3 files changed, 51 insertions(+), 54 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index cf564afacc..198afbf14d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -193,6 +193,8 @@ Additions to existing modules
   //-rightDivides  : RightDivides _∙_ _//_
 
   ⁻¹-selfInverse  : SelfInverse _⁻¹
+  x∙y⁻¹≈ε⇒x≈y     : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y
+  x≈y⇒x∙y⁻¹≈ε     : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε
   \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
   comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x
   ```
@@ -359,9 +361,23 @@ Additions to existing modules
   product-↭ : product Preserves _↭_ ⟶ _≡_
   ```
 
+* In `Data.Rational.Properties`:
+  ```agda
+  1≢0 : 1ℚ ≢ 0ℚ
+
+  #⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q)
+  invertible⇒# : Invertible 1ℚ _*_ (p - q) → p ≢ q
+
+  isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
+  isHeytingField           : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
+  heytingCommutativeRing   : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ
+  heytingField             : HeytingField 0ℓ 0ℓ 0ℓ
+  ```
+
 * Added new functions in `Data.String.Base`:
   ```agda
   map : (Char → Char) → String → String
+  ```
 
 * Added new definition in `Relation.Binary.Construct.Closure.Transitive`
   ```
diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda
index a3733a6ac4..cbb738bff7 100644
--- a/src/Algebra/Properties/Group.agda
+++ b/src/Algebra/Properties/Group.agda
@@ -115,21 +115,18 @@ inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _)
 ⁻¹-involutive : Involutive _⁻¹
 ⁻¹-involutive = selfInverse⇒involutive ⁻¹-selfInverse
 
-x∙y⁻¹≈ε→x≈y : (x y : Carrier) → (x ∙ y ⁻¹) ≈ ε → x ≈ y
-x∙y⁻¹≈ε→x≈y x y x∙y⁻¹≈ε = begin
+x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y
+x∙y⁻¹≈ε⇒x≈y x y x∙y⁻¹≈ε = begin
   x         ≈⟨ inverseˡ-unique x (y ⁻¹) x∙y⁻¹≈ε ⟩
-  y ⁻¹ ⁻¹  ≈⟨ ⁻¹-involutive y ⟩
+  y ⁻¹ ⁻¹   ≈⟨ ⁻¹-involutive y ⟩
   y         ∎
 
-x≈y→x∙y⁻¹≈ε : (x y : Carrier) → x ≈ y → (x ∙ y ⁻¹) ≈ ε
-x≈y→x∙y⁻¹≈ε x y x≈y = begin
+x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε
+x≈y⇒x∙y⁻¹≈ε {x} {y} x≈y = begin
   x ∙ y ⁻¹ ≈⟨ ∙-congʳ x≈y ⟩
   y ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩
   ε        ∎
 
-x≉y→x∙y⁻¹≉ε : (x y : Carrier) → x ≉ y → (x ∙ y ⁻¹) ≉ ε
-x≉y→x∙y⁻¹≉ε x y x≉y x∙y⁻¹≈ε = x≉y (x∙y⁻¹≈ε→x≈y x y x∙y⁻¹≈ε)
-
 ⁻¹-injective : Injective _≈_ _≈_ _⁻¹
 ⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse
 
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 5b79a2eba0..7f22a6f605 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -9,6 +9,7 @@
 
 module Data.Rational.Properties where
 
+open import Algebra.Apartness
 open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
 import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
@@ -21,7 +22,7 @@ import Algebra.Morphism.GroupMonomorphism  as GroupMonomorphisms
 import Algebra.Morphism.RingMonomorphism   as RingMonomorphisms
 import Algebra.Lattice.Morphism.LatticeMonomorphism as LatticeMonomorphisms
 import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties
-open import Algebra.Apartness
+import Algebra.Properties.Group as GroupProperties
 open import Data.Bool.Base using (T; true; false)
 open import Data.Integer.Base as ℤ using (ℤ; +_; -[1+_]; +[1+_]; +0; 0ℤ; 1ℤ; _◃_)
 open import Data.Integer.Coprimality using (coprime-divisor)
@@ -51,13 +52,15 @@ open import Function.Base using (_∘_; _∘′_; _∘₂_; _$_; flip)
 open import Function.Definitions using (Injective)
 open import Level using (0ℓ)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Morphism.Structures
 import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms
+open import Relation.Binary.PropositionalEquality
+import Relation.Binary.Properties.DecSetoid as DecSetoidProperties
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+open import Relation.Binary.Reasoning.Syntax
 open import Relation.Nullary.Decidable.Core as Dec
   using (yes; no; recompute; map′; _×-dec_)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
-open import Relation.Binary.Reasoning.Syntax
 
 open import Algebra.Definitions {A = ℚ} _≡_
 open import Algebra.Structures  {A = ℚ} _≡_
@@ -1248,63 +1251,44 @@ module _ where
   open CommutativeRing +-*-commutativeRing
     using (+-group; zeroˡ; *-congʳ; isCommutativeRing)
 
-  open import Algebra.Properties.Group +-group
-  open import Relation.Binary.Reasoning.Setoid ≡-setoid
-  open import Relation.Binary.Properties.DecSetoid ≡-decSetoid
+  open GroupProperties +-group
+  open DecSetoidProperties ≡-decSetoid
+
+  p*q≡r→p≢0 : r ≢ 0ℚ → p * q ≡ r → p ≢ 0ℚ
+  p*q≡r→p≢0 {r} {p} {q} r≉0 p*q≡r p≡0 = contradiction r≈0 r≉0
+    where
+    open ≈-Reasoning ≡-setoid
+    r≈0 : r ≡ 0ℚ
+    r≈0 = begin
+      r      ≈⟨ p*q≡r ⟨
+      p * q  ≈⟨ *-congʳ p≡0 ⟩
+      0ℚ * q ≈⟨ zeroˡ q ⟩
+      0ℚ     ∎
+
+  #⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q)
+  #⇒invertible {p} {q} p≢q = let r = p - q in 1/ r , *-inverseˡ r , *-inverseʳ r
+    where instance _ = ≢-nonZero (p≢q ∘ (x∙y⁻¹≈ε⇒x≈y p q))
+
+  invertible⇒# : Invertible 1ℚ _*_ (p - q) → p ≢ q
+  invertible⇒# {p} {q} (1/[p-q] , _ , [p-q]/[p-q]≡1) p≡q =
+    p*q≡r→p≢0 1≢0 [p-q]/[p-q]≡1 (x≈y⇒x∙y⁻¹≈ε p≡q)
 
   isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
-  isHeytingCommutativeRing =
-    record
+  isHeytingCommutativeRing = record
     { isCommutativeRing = isCommutativeRing
     ; isApartnessRelation = ≉-isApartnessRelation
     ; #⇒invertible = #⇒invertible
     ; invertible⇒# = invertible⇒#
     }
-    where
-      x*y≡z→x≢0 : ∀ x y z → z ≢ 0ℚ → x * y ≡ z → x ≢ 0ℚ
-      x*y≡z→x≢0 x y z z≉0 x*y≡z x≡0 =
-        z≉0
-        $ begin
-            z
-          ≈⟨ sym x*y≡z ⟩
-            x * y
-          ≈⟨ *-congʳ x≡0 ⟩
-            0ℚ * y
-          ≈⟨ zeroˡ y ⟩
-            0ℚ
-          ∎
-        where
-          open import Function using (_$_)
-
-      #⇒invertible : {x y : ℚ} → x ≢ y → Invertible 1ℚ _*_ (x - y)
-      #⇒invertible {x} {y} x≢y =
-        let instance _ = ≢-nonZero (x≉y→x∙y⁻¹≉ε x y x≢y)
-        in
-          ( 1/_ (x - y)
-          , *-inverseˡ (x - y)
-          , *-inverseʳ (x - y)
-          )
-
-      invertible⇒# : ∀ {i j} → Invertible 1ℚ _*_ (i - j) → i ≢ j
-      invertible⇒# {i} {j} (1/[i-j] , _ , [i-j]/[i-j]≡1) i≡j =
-        x*y≡z→x≢0
-          (i - j)
-          1/[i-j]
-          1ℚ
-          1≢0
-          [i-j]/[i-j]≡1
-          (x≈y→x∙y⁻¹≈ε i j i≡j)
 
   isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
-  isHeytingField =
-    record
+  isHeytingField = record
     { isHeytingCommutativeRing = isHeytingCommutativeRing
     ; tight = ≉-tight
     }
 
   heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ
-  heytingCommutativeRing =
-    record { isHeytingCommutativeRing = isHeytingCommutativeRing }
+  heytingCommutativeRing = record { isHeytingCommutativeRing = isHeytingCommutativeRing }
 
   heytingField : HeytingField 0ℓ 0ℓ 0ℓ
   heytingField = record { isHeytingField = isHeytingField }

From 7459d22346a49c296b8857aeccdddbf8de8809c9 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Thu, 16 May 2024 16:14:23 +0100
Subject: [PATCH 14/14] inlined lemma; tidied up

---
 src/Data/Rational/Properties.agda | 25 +++++++++++--------------
 1 file changed, 11 insertions(+), 14 deletions(-)

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 7f22a6f605..3c959bda84 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -1246,7 +1246,8 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i
 
 
 ------------------------------------------------------------------------
--- Field-like structures and bundles
+-- HeytingField structures and bundles
+
 module _ where
   open CommutativeRing +-*-commutativeRing
     using (+-group; zeroˡ; *-congʳ; isCommutativeRing)
@@ -1254,24 +1255,20 @@ module _ where
   open GroupProperties +-group
   open DecSetoidProperties ≡-decSetoid
 
-  p*q≡r→p≢0 : r ≢ 0ℚ → p * q ≡ r → p ≢ 0ℚ
-  p*q≡r→p≢0 {r} {p} {q} r≉0 p*q≡r p≡0 = contradiction r≈0 r≉0
-    where
-    open ≈-Reasoning ≡-setoid
-    r≈0 : r ≡ 0ℚ
-    r≈0 = begin
-      r      ≈⟨ p*q≡r ⟨
-      p * q  ≈⟨ *-congʳ p≡0 ⟩
-      0ℚ * q ≈⟨ zeroˡ q ⟩
-      0ℚ     ∎
-
   #⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q)
   #⇒invertible {p} {q} p≢q = let r = p - q in 1/ r , *-inverseˡ r , *-inverseʳ r
     where instance _ = ≢-nonZero (p≢q ∘ (x∙y⁻¹≈ε⇒x≈y p q))
 
   invertible⇒# : Invertible 1ℚ _*_ (p - q) → p ≢ q
-  invertible⇒# {p} {q} (1/[p-q] , _ , [p-q]/[p-q]≡1) p≡q =
-    p*q≡r→p≢0 1≢0 [p-q]/[p-q]≡1 (x≈y⇒x∙y⁻¹≈ε p≡q)
+  invertible⇒# {p} {q} (1/[p-q] , _ , [p-q]/[p-q]≡1) p≡q = contradiction 1≡0 1≢0
+    where
+    open ≈-Reasoning ≡-setoid
+    1≡0 : 1ℚ ≡ 0ℚ
+    1≡0 = begin
+      1ℚ                 ≈⟨ [p-q]/[p-q]≡1 ⟨
+      (p - q) * 1/[p-q]  ≈⟨ *-congʳ (x≈y⇒x∙y⁻¹≈ε p≡q) ⟩
+      0ℚ * 1/[p-q]       ≈⟨ zeroˡ 1/[p-q] ⟩
+      0ℚ                 ∎
 
   isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
   isHeytingCommutativeRing = record