From d17104288c517418e88eac5f86354dc56a1ba4b3 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 18 Feb 2025 12:18:09 +0000
Subject: [PATCH 01/14] refactor: fix #2587

---
 CHANGELOG.md                                  |  4 ++++
 src/Algebra/Apartness/Bundles.agda            | 10 ++++-----
 src/Algebra/Apartness/Structures.agda         | 22 +++++++++----------
 src/Data/Rational/Properties.agda             |  7 +++---
 .../Rational/Unnormalised/Properties.agda     | 18 +++++++++------
 src/Relation/Binary/Bundles.agda              | 15 +++++++++++++
 src/Relation/Binary/Definitions.agda          |  2 +-
 src/Relation/Binary/Properties/DecSetoid.agda |  2 +-
 src/Relation/Binary/Structures.agda           |  7 ++++++
 9 files changed, 57 insertions(+), 30 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f13d2635cb..72272404c4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,6 +17,10 @@ Non-backwards compatible changes
   significantly faster. However, its reduction behaviour on open terms may have
   changed.
 
+* The definitions of `Algebra.Structures.IsHeytingCommutativeRing` and
+  `Algebra.Structures.IsHeytingCommutativeRing` have been refactored, together
+  with that of `Relation.Binary.Definitions.Tight` on which they depend.
+
 Minor improvements
 ------------------
 
diff --git a/src/Algebra/Apartness/Bundles.agda b/src/Algebra/Apartness/Bundles.agda
index 9a55794051..ff6768b873 100644
--- a/src/Algebra/Apartness/Bundles.agda
+++ b/src/Algebra/Apartness/Bundles.agda
@@ -10,7 +10,7 @@ module Algebra.Apartness.Bundles where
 
 open import Level using (_⊔_; suc)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Bundles using (ApartnessRelation)
+open import Relation.Binary.Bundles using (TightApartnessRelation)
 open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Bundles using (CommutativeRing)
 open import Algebra.Apartness.Structures
@@ -36,8 +36,8 @@ record HeytingCommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ
   commutativeRing : CommutativeRing c ℓ₁
   commutativeRing = record { isCommutativeRing = isCommutativeRing }
 
-  apartnessRelation : ApartnessRelation c ℓ₁ ℓ₂
-  apartnessRelation = record { isApartnessRelation = isApartnessRelation }
+  tightApartnessRelation : TightApartnessRelation c ℓ₁ ℓ₂
+  tightApartnessRelation = record { isTightApartnessRelation = isTightApartnessRelation }
 
 
 record HeytingField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -61,5 +61,5 @@ record HeytingField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   heytingCommutativeRing : HeytingCommutativeRing c ℓ₁ ℓ₂
   heytingCommutativeRing = record { isHeytingCommutativeRing = isHeytingCommutativeRing }
 
-  apartnessRelation : ApartnessRelation c ℓ₁ ℓ₂
-  apartnessRelation = record { isApartnessRelation = isApartnessRelation }
+  open HeytingCommutativeRing heytingCommutativeRing public
+    using (commutativeRing; tightApartnessRelation)
diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda
index a8c5c88982..581a0c2db7 100644
--- a/src/Algebra/Apartness/Structures.agda
+++ b/src/Algebra/Apartness/Structures.agda
@@ -17,27 +17,21 @@ module Algebra.Apartness.Structures
   where
 
 open import Level using (_⊔_; suc)
-open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₂)
 open import Algebra.Definitions _≈_ using (Invertible)
 open import Algebra.Structures _≈_ using (IsCommutativeRing)
-open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation)
-open import Relation.Binary.Definitions using (Tight)
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Binary.Structures
+  using (IsEquivalence; IsApartnessRelation; IsTightApartnessRelation)
 import Relation.Binary.Properties.ApartnessRelation as AR
 
 
 record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
 
   field
-    isCommutativeRing   : IsCommutativeRing _+_ _*_ -_ 0# 1#
-    isApartnessRelation : IsApartnessRelation _≈_ _#_
+    isCommutativeRing        : IsCommutativeRing _+_ _*_ -_ 0# 1#
+    isTightApartnessRelation : IsTightApartnessRelation _≈_ _#_
 
   open IsCommutativeRing isCommutativeRing public
-  open IsApartnessRelation isApartnessRelation public
-
-  field
-    #⇒invertible : ∀ {x y} → x # y → Invertible 1# _*_ (x - y)
-    invertible⇒# : ∀ {x y} → Invertible 1# _*_ (x - y) → x # y
+  open IsTightApartnessRelation isTightApartnessRelation public
 
   ¬#-isEquivalence : IsEquivalence _¬#_
   ¬#-isEquivalence = AR.¬#-isEquivalence refl isApartnessRelation
@@ -47,6 +41,10 @@ record IsHeytingField : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
 
   field
     isHeytingCommutativeRing : IsHeytingCommutativeRing
-    tight                    : Tight _≈_ _#_
 
   open IsHeytingCommutativeRing isHeytingCommutativeRing public
+
+  field
+    #⇒invertible             : ∀ {x y} → x # y → Invertible 1# _*_ (x - y)
+    invertible⇒#             : ∀ {x y} → Invertible 1# _*_ (x - y) → x # y
+
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 0341f53c45..ab739053e1 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -1299,15 +1299,14 @@ module _ where
   isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
   isHeytingCommutativeRing = record
     { isCommutativeRing = isCommutativeRing
-    ; isApartnessRelation = ≉-isApartnessRelation
-    ; #⇒invertible = #⇒invertible
-    ; invertible⇒# = invertible⇒#
+    ; isTightApartnessRelation = ≉-isTightApartnessRelation
     }
 
   isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
   isHeytingField = record
     { isHeytingCommutativeRing = isHeytingCommutativeRing
-    ; tight = ≉-tight
+    ; #⇒invertible = #⇒invertible
+    ; invertible⇒# = invertible⇒#
     }
 
   heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 11e8d917b1..cf4c461fec 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -35,7 +35,7 @@ open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder; DenseLinearOrder)
 open import Relation.Binary.Structures
-  using (IsEquivalence; IsDecEquivalence; IsApartnessRelation; IsTotalPreorder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder; IsDenseLinearOrder)
+  using (IsEquivalence; IsDecEquivalence; IsApartnessRelation; IsTightApartnessRelation; IsTotalPreorder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder; IsDenseLinearOrder)
 open import Relation.Binary.Definitions
   using (Reflexive; Symmetric; Transitive; Cotransitive; Tight; Decidable; Antisymmetric; Asymmetric; Dense; Total; Trans; Trichotomous; Irreflexive; Irrelevant; _Respectsˡ_; _Respectsʳ_; _Respects₂_; tri≈; tri<; tri>)
 import Relation.Binary.Consequences as BC
@@ -139,8 +139,13 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* 
   }
 
 ≄-tight : Tight _≃_ _≄_
-proj₁ (≄-tight p q) ¬p≄q = Dec.decidable-stable (p ≃? q) ¬p≄q
-proj₂ (≄-tight p q) p≃q p≄q = p≄q p≃q
+≄-tight p q = Dec.decidable-stable (p ≃? q)
+
+≄-isTightApartnessRelation : IsTightApartnessRelation _≃_ _≄_
+≄-isTightApartnessRelation = record
+  { isApartnessRelation = ≄-isApartnessRelation
+  ; tight = ≄-tight
+  }
 
 ≃-setoid : Setoid 0ℓ 0ℓ
 ≃-setoid = record
@@ -1399,15 +1404,14 @@ nonNeg*nonNeg⇒nonNeg p q = nonNegative
 +-*-isHeytingCommutativeRing : IsHeytingCommutativeRing _≃_ _≄_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
 +-*-isHeytingCommutativeRing = record
   { isCommutativeRing   = +-*-isCommutativeRing
-  ; isApartnessRelation = ≄-isApartnessRelation
-  ; #⇒invertible        = ≄⇒invertible
-  ; invertible⇒#        = invertible⇒≄
+  ; isTightApartnessRelation = ≄-isTightApartnessRelation
   }
 
 +-*-isHeytingField : IsHeytingField _≃_ _≄_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
 +-*-isHeytingField = record
   { isHeytingCommutativeRing = +-*-isHeytingCommutativeRing
-  ; tight                    = ≄-tight
+  ; #⇒invertible        = ≄⇒invertible
+  ; invertible⇒#        = invertible⇒≄
   }
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda
index f471cf7bd4..f3edd76ce7 100644
--- a/src/Relation/Binary/Bundles.agda
+++ b/src/Relation/Binary/Bundles.agda
@@ -424,3 +424,18 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
     renaming (_≁_ to _¬#_; _∼ᵒ_ to _#ᵒ_; _≁ᵒ_ to _¬#ᵒ_)
     hiding (Carrier; _≈_ ; _∼_)
 
+record TightApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _#_
+  field
+    Carrier                  : Set c
+    _≈_                      : Rel Carrier ℓ₁
+    _#_                      : Rel Carrier ℓ₂
+    isTightApartnessRelation : IsTightApartnessRelation _≈_ _#_
+
+  open IsTightApartnessRelation isTightApartnessRelation public
+    using (isApartnessRelation; tight)
+
+  apartnessRelation : ApartnessRelation _ _ _
+  apartnessRelation = record { isApartnessRelation = isApartnessRelation }
+
+  open ApartnessRelation apartnessRelation public
diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda
index 167b63a8cb..210ebd0f4e 100644
--- a/src/Relation/Binary/Definitions.agda
+++ b/src/Relation/Binary/Definitions.agda
@@ -147,7 +147,7 @@ Cotransitive : Rel A ℓ → Set _
 Cotransitive _#_ = ∀ {x y} → x # y → ∀ z → (x # z) ⊎ (z # y)
 
 Tight : Rel A ℓ₁ → Rel A ℓ₂ → Set _
-Tight _≈_ _#_ = ∀ x y → (¬ x # y → x ≈ y) × (x ≈ y → ¬ x # y)
+Tight _≈_ _#_ = ∀ x y → ¬ x # y → x ≈ y
 
 -- Properties of order morphisms, aka order-preserving maps
 
diff --git a/src/Relation/Binary/Properties/DecSetoid.agda b/src/Relation/Binary/Properties/DecSetoid.agda
index 7f9b323d85..6e2eef2a1a 100644
--- a/src/Relation/Binary/Properties/DecSetoid.agda
+++ b/src/Relation/Binary/Properties/DecSetoid.agda
@@ -40,4 +40,4 @@ open SetoidProperties setoid
 ≉-apartnessRelation = record { isApartnessRelation = ≉-isApartnessRelation }
 
 ≉-tight : Tight _≈_ _≉_
-≉-tight x y = decidable-stable (x ≟ y) , ≉-irrefl
+≉-tight x y = decidable-stable (x ≟ y)
diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda
index 3bbfc6db27..f0d2665593 100644
--- a/src/Relation/Binary/Structures.agda
+++ b/src/Relation/Binary/Structures.agda
@@ -328,3 +328,10 @@ record IsApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) whe
 
   _¬#_ : A → A → Set _
   x ¬# y = ¬ (x # y)
+
+record IsTightApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isApartnessRelation : IsApartnessRelation _#_
+    tight               : Tight _≈_ _#_
+
+  open IsApartnessRelation isApartnessRelation public

From d07718cc02d416385179df5db32cb3ad37e4dae3 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 18 Feb 2025 12:43:15 +0000
Subject: [PATCH 02/14] refactor: properties of `HeytingField`, not
 `HeytingCommutativeRing`

---
 .../Properties/HeytingCommutativeRing.agda    |  92 +--------------
 .../Apartness/Properties/HeytingField.agda    | 108 ++++++++++++++++++
 2 files changed, 112 insertions(+), 88 deletions(-)
 create mode 100644 src/Algebra/Apartness/Properties/HeytingField.agda

diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
index d8b3ffcdfd..6f7f54bfad 100644
--- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
+++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
@@ -11,98 +11,14 @@ open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
 module Algebra.Apartness.Properties.HeytingCommutativeRing
   {c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where
 
-open import Function.Base using (_∘_)
-open import Data.Product.Base using (_,_; proj₁; proj₂)
-open import Algebra using (CommutativeRing; RightIdentity; Invertible; LeftInvertible; RightInvertible)
+open import Algebra using (CommutativeRing; RightIdentity)
 
 open HeytingCommutativeRing HCR
-open CommutativeRing commutativeRing using (ring; *-commutativeMonoid)
-
-open import Algebra.Properties.Ring ring
-  using (-0#≈0#; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive)
-open import Relation.Binary.Definitions using (Symmetric)
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid
+open CommutativeRing commutativeRing using (ring)
+open import Algebra.Properties.Ring ring using (-0#≈0#)
 
 private variable
-  x y z : Carrier
-
-invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y
-invertibleˡ⇒# = invertible⇒# ∘ invertibleˡ⇒invertible
-
-invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y
-invertibleʳ⇒# = invertible⇒# ∘ invertibleʳ⇒invertible
+  x : Carrier
 
 x-0≈x : RightIdentity _≈_ 0# _-_
 x-0≈x x = trans (+-congˡ -0#≈0#) (+-identityʳ x)
-
-1#0 : 1# # 0#
-1#0 = invertibleˡ⇒# (1# , 1*[x-0]≈x)
-  where
-  1*[x-0]≈x : 1# * (x - 0#) ≈ x
-  1*[x-0]≈x {x} = trans (*-identityˡ (x - 0#)) (x-0≈x x)
-
-x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0#
-x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
-  where
-
-  helper : Invertible _≈_ 1# _*_ (x - 0#) → Invertible _≈_ 1# _*_ (y - 0#) → x * y # 0#
-  helper (x⁻¹ , x⁻¹*x≈1 , x*x⁻¹≈1) (y⁻¹ , y⁻¹*y≈1 , y*y⁻¹≈1)
-    = invertibleˡ⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1)
-    where
-    open ≈-Reasoning setoid
-
-    y⁻¹*x⁻¹*x*y≈1 : y⁻¹ * x⁻¹ * (x * y - 0#) ≈ 1#
-    y⁻¹*x⁻¹*x*y≈1 = begin
-      y⁻¹ * x⁻¹ * (x * y - 0#)     ≈⟨ *-congˡ (x-0≈x (x * y)) ⟩
-      y⁻¹ * x⁻¹ * (x * y)          ≈⟨ *-assoc y⁻¹ x⁻¹ (x * y) ⟩
-      y⁻¹ * (x⁻¹ * (x * y))       ≈⟨ *-congˡ (*-assoc x⁻¹ x y) ⟨
-      y⁻¹ * ((x⁻¹ * x) * y)       ≈⟨ *-congˡ (*-congʳ (*-congˡ (x-0≈x x))) ⟨
-      y⁻¹ * ((x⁻¹ * (x - 0#)) * y) ≈⟨ *-congˡ (*-congʳ x⁻¹*x≈1) ⟩
-      y⁻¹ * (1# * y)               ≈⟨ *-congˡ (*-identityˡ y) ⟩
-      y⁻¹ * y                     ≈⟨ *-congˡ (x-0≈x y) ⟨
-      y⁻¹ * (y - 0#)               ≈⟨ y⁻¹*y≈1 ⟩
-      1# ∎
-
-#-sym : Symmetric _#_
-#-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1)
-  where
-  open ≈-Reasoning setoid
-  InvX-Y : Invertible _≈_ 1# _*_ (x - y)
-  InvX-Y = #⇒invertible x#y
-
-  x-y⁻¹ = InvX-Y .proj₁
-
-  y-x≈-[x-y] : y - x ≈ - (x - y)
-  y-x≈-[x-y] = begin
-    y - x     ≈⟨ +-congʳ (-‿involutive y) ⟨
-    - - y - x ≈⟨ -‿anti-homo-+ x (- y) ⟨
-    - (x - y) ∎
-
-  x-y⁻¹*y-x≈1 : (- x-y⁻¹) * (y - x) ≈ 1#
-  x-y⁻¹*y-x≈1 = begin
-    (- x-y⁻¹) * (y - x)   ≈⟨ -‿distribˡ-* x-y⁻¹ (y - x) ⟨
-    - (x-y⁻¹ * (y - x))    ≈⟨ -‿cong (*-congˡ y-x≈-[x-y]) ⟩
-    - (x-y⁻¹ * - (x - y)) ≈⟨ -‿cong (-‿distribʳ-* x-y⁻¹ (x - y)) ⟨
-    - - (x-y⁻¹ * (x - y))  ≈⟨ -‿involutive (x-y⁻¹ * ((x - y))) ⟩
-    x-y⁻¹ * (x - y)        ≈⟨ InvX-Y .proj₂ .proj₁ ⟩
-    1# ∎
-
-#-congʳ : x ≈ y → x # z → y # z
-#-congʳ {x} {y} {z} x≈y x#z = helper (#⇒invertible x#z)
-  where
-
-  helper : Invertible _≈_ 1# _*_ (x - z) → y # z
-  helper (x-z⁻¹ , x-z⁻¹*x-z≈1# , x-z*x-z⁻¹≈1#)
-    = invertibleˡ⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1)
-    where
-    open ≈-Reasoning setoid
-
-    x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1#
-    x-z⁻¹*y-z≈1 = begin
-      x-z⁻¹ * (y - z) ≈⟨ *-congˡ (+-congʳ x≈y) ⟨
-      x-z⁻¹ * (x - z)  ≈⟨ x-z⁻¹*x-z≈1# ⟩
-      1# ∎
-
-#-congˡ : y ≈ z → x # y → x # z
-#-congˡ y≈z x#y = #-sym (#-congʳ y≈z (#-sym x#y))
diff --git a/src/Algebra/Apartness/Properties/HeytingField.agda b/src/Algebra/Apartness/Properties/HeytingField.agda
new file mode 100644
index 0000000000..a9588c3b20
--- /dev/null
+++ b/src/Algebra/Apartness/Properties/HeytingField.agda
@@ -0,0 +1,108 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of Heyting Commutative Rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Apartness.Bundles using (HeytingCommutativeRing; HeytingField)
+
+module Algebra.Apartness.Properties.HeytingField
+  {c ℓ₁ ℓ₂} (HF : HeytingField c ℓ₁ ℓ₂) where
+
+open import Function.Base using (_∘_)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Algebra using (CommutativeRing; RightIdentity; Invertible; LeftInvertible; RightInvertible)
+
+open HeytingField HF
+open CommutativeRing commutativeRing using (ring; *-commutativeMonoid)
+
+open import Algebra.Properties.Ring ring
+  using (-0#≈0#; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive)
+open import Relation.Binary.Definitions using (Symmetric)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid
+
+private variable
+  x y z : Carrier
+
+
+open import Algebra.Apartness.Properties.HeytingCommutativeRing heytingCommutativeRing public
+
+invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y
+invertibleˡ⇒# = invertible⇒# ∘ invertibleˡ⇒invertible
+
+invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y
+invertibleʳ⇒# = invertible⇒# ∘ invertibleʳ⇒invertible
+
+1#0 : 1# # 0#
+1#0 = invertibleˡ⇒# (1# , 1*[x-0]≈x)
+  where
+  1*[x-0]≈x : 1# * (x - 0#) ≈ x
+  1*[x-0]≈x {x} = trans (*-identityˡ (x - 0#)) (x-0≈x x)
+
+x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0#
+x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
+  where
+
+  helper : Invertible _≈_ 1# _*_ (x - 0#) → Invertible _≈_ 1# _*_ (y - 0#) → x * y # 0#
+  helper (x⁻¹ , x⁻¹*x≈1 , x*x⁻¹≈1) (y⁻¹ , y⁻¹*y≈1 , y*y⁻¹≈1)
+    = invertibleˡ⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1)
+    where
+    open ≈-Reasoning setoid
+
+    y⁻¹*x⁻¹*x*y≈1 : y⁻¹ * x⁻¹ * (x * y - 0#) ≈ 1#
+    y⁻¹*x⁻¹*x*y≈1 = begin
+      y⁻¹ * x⁻¹ * (x * y - 0#)     ≈⟨ *-congˡ (x-0≈x (x * y)) ⟩
+      y⁻¹ * x⁻¹ * (x * y)          ≈⟨ *-assoc y⁻¹ x⁻¹ (x * y) ⟩
+      y⁻¹ * (x⁻¹ * (x * y))       ≈⟨ *-congˡ (*-assoc x⁻¹ x y) ⟨
+      y⁻¹ * ((x⁻¹ * x) * y)       ≈⟨ *-congˡ (*-congʳ (*-congˡ (x-0≈x x))) ⟨
+      y⁻¹ * ((x⁻¹ * (x - 0#)) * y) ≈⟨ *-congˡ (*-congʳ x⁻¹*x≈1) ⟩
+      y⁻¹ * (1# * y)               ≈⟨ *-congˡ (*-identityˡ y) ⟩
+      y⁻¹ * y                     ≈⟨ *-congˡ (x-0≈x y) ⟨
+      y⁻¹ * (y - 0#)               ≈⟨ y⁻¹*y≈1 ⟩
+      1# ∎
+
+#-sym : Symmetric _#_
+#-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1)
+  where
+  open ≈-Reasoning setoid
+  InvX-Y : Invertible _≈_ 1# _*_ (x - y)
+  InvX-Y = #⇒invertible x#y
+
+  x-y⁻¹ = InvX-Y .proj₁
+
+  y-x≈-[x-y] : y - x ≈ - (x - y)
+  y-x≈-[x-y] = begin
+    y - x     ≈⟨ +-congʳ (-‿involutive y) ⟨
+    - - y - x ≈⟨ -‿anti-homo-+ x (- y) ⟨
+    - (x - y) ∎
+
+  x-y⁻¹*y-x≈1 : (- x-y⁻¹) * (y - x) ≈ 1#
+  x-y⁻¹*y-x≈1 = begin
+    (- x-y⁻¹) * (y - x)   ≈⟨ -‿distribˡ-* x-y⁻¹ (y - x) ⟨
+    - (x-y⁻¹ * (y - x))    ≈⟨ -‿cong (*-congˡ y-x≈-[x-y]) ⟩
+    - (x-y⁻¹ * - (x - y)) ≈⟨ -‿cong (-‿distribʳ-* x-y⁻¹ (x - y)) ⟨
+    - - (x-y⁻¹ * (x - y))  ≈⟨ -‿involutive (x-y⁻¹ * ((x - y))) ⟩
+    x-y⁻¹ * (x - y)        ≈⟨ InvX-Y .proj₂ .proj₁ ⟩
+    1# ∎
+
+#-congʳ : x ≈ y → x # z → y # z
+#-congʳ {x} {y} {z} x≈y x#z = helper (#⇒invertible x#z)
+  where
+
+  helper : Invertible _≈_ 1# _*_ (x - z) → y # z
+  helper (x-z⁻¹ , x-z⁻¹*x-z≈1# , x-z*x-z⁻¹≈1#)
+    = invertibleˡ⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1)
+    where
+    open ≈-Reasoning setoid
+
+    x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1#
+    x-z⁻¹*y-z≈1 = begin
+      x-z⁻¹ * (y - z) ≈⟨ *-congˡ (+-congʳ x≈y) ⟨
+      x-z⁻¹ * (x - z)  ≈⟨ x-z⁻¹*x-z≈1# ⟩
+      1# ∎
+
+#-congˡ : y ≈ z → x # y → x # z
+#-congˡ y≈z x#y = #-sym (#-congʳ y≈z (#-sym x#y))

From 7f2f4af536bb6d4c9c62d421089a0c4db10600ad Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 18 Feb 2025 13:07:44 +0000
Subject: [PATCH 03/14] refactor: give `DecSetoid`s the structure of
 `(Is)TightApartnessRelation`

---
 CHANGELOG.md                                  | 24 +++++++++++++++++--
 src/Data/Rational/Properties.agda             |  2 +-
 src/Relation/Binary/Properties/DecSetoid.agda | 20 ++++++++++++----
 3 files changed, 39 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 72272404c4..a0b43bbcb5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,8 +17,8 @@ Non-backwards compatible changes
   significantly faster. However, its reduction behaviour on open terms may have
   changed.
 
-* The definitions of `Algebra.Structures.IsHeytingCommutativeRing` and
-  `Algebra.Structures.IsHeytingCommutativeRing` have been refactored, together
+* The definitions of `Algebra.Structures.IsHeyting*` and
+  `Algebra.Structures.IsHeyting*` have been refactored, together
   with that of `Relation.Binary.Definitions.Tight` on which they depend.
 
 Minor improvements
@@ -95,6 +95,9 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Apartness.Properties.HeytingField`, refactoring the existing
+  `Algebra.Apartness.Properties.HeytingCommutativeRing`.
+
 * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`.
 
 * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
@@ -102,6 +105,16 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Apartness.Bundles`:
+  ```agda
+  TightApartnessRelation c ℓ₁ ℓ₂ : Set _
+  ```
+
+* In `Algebra.Apartness.Structures`:
+  ```agda
+  IsTightApartnessRelation _≈_ _#_ : Set _
+  ```
+
 * In `Algebra.Construct.Pointwise`:
   ```agda
   isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →
@@ -130,3 +143,10 @@ Additions to existing modules
   quasiring                       : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
+
+* In `Relation.Binary.Properties.DecSetoid`:
+  ```agda
+  ≉-isTightApartnessRelation : IsTightApartnessRelation _≈_ _#_
+  ≉-tightApartnessRelation   : TightApartnessRelation _ _ _
+  ```
+
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index ab739053e1..27863543e5 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -1299,7 +1299,7 @@ module _ where
   isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
   isHeytingCommutativeRing = record
     { isCommutativeRing = isCommutativeRing
-    ; isTightApartnessRelation = ≉-isTightApartnessRelation
+    ; isTightApartnessRelation = {!≉-isTightApartnessRelation!}
     }
 
   isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
diff --git a/src/Relation/Binary/Properties/DecSetoid.agda b/src/Relation/Binary/Properties/DecSetoid.agda
index 6e2eef2a1a..44fd2012e5 100644
--- a/src/Relation/Binary/Properties/DecSetoid.agda
+++ b/src/Relation/Binary/Properties/DecSetoid.agda
@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Bundles using (DecSetoid; ApartnessRelation)
+open import Relation.Binary.Bundles
+  using (DecSetoid; ApartnessRelation; TightApartnessRelation)
 
 module Relation.Binary.Properties.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where
 
@@ -16,7 +17,7 @@ open import Relation.Binary.Definitions
   using (Cotransitive; Tight)
 import Relation.Binary.Properties.Setoid as SetoidProperties
 open import Relation.Binary.Structures
-  using (IsApartnessRelation; IsDecEquivalence)
+  using (IsApartnessRelation; IsTightApartnessRelation; IsDecEquivalence)
 open import Relation.Nullary.Decidable.Core
   using (yes; no; decidable-stable)
 
@@ -36,8 +37,19 @@ open SetoidProperties setoid
   ; cotrans = ≉-cotrans
   }
 
+≉-tight : Tight _≈_ _≉_
+≉-tight x y = decidable-stable (x ≟ y)
+
+≉-isTightApartnessRelation : IsTightApartnessRelation _≈_ _≉_
+≉-isTightApartnessRelation = record
+  { isApartnessRelation = ≉-isApartnessRelation
+  ; tight = ≉-tight
+  }
+
 ≉-apartnessRelation : ApartnessRelation c ℓ ℓ
 ≉-apartnessRelation = record { isApartnessRelation = ≉-isApartnessRelation }
 
-≉-tight : Tight _≈_ _≉_
-≉-tight x y = decidable-stable (x ≟ y)
+≉-tightApartnessRelation : TightApartnessRelation c ℓ ℓ
+≉-tightApartnessRelation = record
+  { isTightApartnessRelation = ≉-isTightApartnessRelation }
+

From 408433dfbe192832e33638eab635be3d85bbd5a4 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 18 Feb 2025 13:19:39 +0000
Subject: [PATCH 04/14] fix: unsaved commits

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

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 27863543e5..ab739053e1 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -1299,7 +1299,7 @@ module _ where
   isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
   isHeytingCommutativeRing = record
     { isCommutativeRing = isCommutativeRing
-    ; isTightApartnessRelation = {!≉-isTightApartnessRelation!}
+    ; isTightApartnessRelation = ≉-isTightApartnessRelation
     }
 
   isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ

From 92f82488bba53ecdba083cf8f34287fc5c16de26 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 09:22:22 +0000
Subject: [PATCH 05/14] =?UTF-8?q?refactor:=20move=20property=20`x-0?=
 =?UTF-8?q?=E2=89=88x`=20to=20`Algebra.Properties.AbelianGroup`,=20re-expo?=
 =?UTF-8?q?rted=20by=20`Algebra.Properties.Ring`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Algebra/Properties/AbelianGroup.agda   | 6 +++++-
 src/Algebra/Properties/RingWithoutOne.agda | 1 +
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Algebra/Properties/AbelianGroup.agda b/src/Algebra/Properties/AbelianGroup.agda
index b5eb290081..2b52c6c755 100644
--- a/src/Algebra/Properties/AbelianGroup.agda
+++ b/src/Algebra/Properties/AbelianGroup.agda
@@ -6,12 +6,13 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
+open import Algebra.Bundles using (AbelianGroup)
 
 module Algebra.Properties.AbelianGroup
   {a ℓ} (G : AbelianGroup a ℓ) where
 
 open AbelianGroup G
+open import Algebra.Definitions _≈_ using (RightIdentity)
 open import Function.Base using (_$_)
 open import Relation.Binary.Reasoning.Setoid setoid
 
@@ -39,3 +40,6 @@ xyx⁻¹≈y x y = begin
   x ⁻¹ ∙ y ⁻¹ ≈⟨ ⁻¹-anti-homo-∙ y x ⟨
   (y ∙ x) ⁻¹  ≈⟨ ⁻¹-cong $ comm y x ⟩
   (x ∙ y) ⁻¹  ∎
+
+x-ε≈x : RightIdentity ε _-_
+x-ε≈x x = trans (∙-congˡ ε⁻¹≈ε) (identityʳ x)
diff --git a/src/Algebra/Properties/RingWithoutOne.agda b/src/Algebra/Properties/RingWithoutOne.agda
index d81ef58477..790136c57f 100644
--- a/src/Algebra/Properties/RingWithoutOne.agda
+++ b/src/Algebra/Properties/RingWithoutOne.agda
@@ -22,6 +22,7 @@ open import Relation.Binary.Reasoning.Setoid setoid
 open AbelianGroupProperties +-abelianGroup public
   renaming
   ( ε⁻¹≈ε            to -0#≈0#
+  ; x-ε≈x            to x-0#≈x
   ; ∙-cancelˡ        to +-cancelˡ
   ; ∙-cancelʳ        to +-cancelʳ
   ; ∙-cancel         to +-cancel

From 55a7384a4bf61aa932c4000269444d9e81c726ef Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 09:28:16 +0000
Subject: [PATCH 06/14] refactor: deprecate and tighten `import`s

---
 .../Properties/HeytingCommutativeRing.agda    | 20 +++++--
 .../Apartness/Properties/HeytingField.agda    | 58 +++++++++----------
 2 files changed, 43 insertions(+), 35 deletions(-)

diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
index 6f7f54bfad..0bdec58432 100644
--- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
+++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
@@ -11,14 +11,22 @@ open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
 module Algebra.Apartness.Properties.HeytingCommutativeRing
   {c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where
 
-open import Algebra using (CommutativeRing; RightIdentity)
+open import Algebra.Bundles using (CommutativeRing)
 
 open HeytingCommutativeRing HCR
 open CommutativeRing commutativeRing using (ring)
-open import Algebra.Properties.Ring ring using (-0#≈0#)
+open import Algebra.Properties.Ring ring using (x-0#≈x)
 
-private variable
-  x : Carrier
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
 
-x-0≈x : RightIdentity _≈_ 0# _-_
-x-0≈x x = trans (+-congˡ -0#≈0#) (+-identityʳ x)
+x-0≈x = x-0#≈x
+{-# WARNING_ON_USAGE x-0≈x
+"Warning: x-0≈x was deprecated in v2.3.
+Please use Algebra.Properties.Ring.x-0#≈x instead."
+#-}
diff --git a/src/Algebra/Apartness/Properties/HeytingField.agda b/src/Algebra/Apartness/Properties/HeytingField.agda
index a9588c3b20..b341b12e6e 100644
--- a/src/Algebra/Apartness/Properties/HeytingField.agda
+++ b/src/Algebra/Apartness/Properties/HeytingField.agda
@@ -1,74 +1,75 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Properties of Heyting Commutative Rings
+-- Properties of Heyting Fields
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Apartness.Bundles using (HeytingCommutativeRing; HeytingField)
+open import Algebra.Apartness.Bundles using (HeytingField)
 
 module Algebra.Apartness.Properties.HeytingField
   {c ℓ₁ ℓ₂} (HF : HeytingField c ℓ₁ ℓ₂) where
 
 open import Function.Base using (_∘_)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
-open import Algebra using (CommutativeRing; RightIdentity; Invertible; LeftInvertible; RightInvertible)
+open import Algebra.Bundles using (CommutativeRing)
 
 open HeytingField HF
 open CommutativeRing commutativeRing using (ring; *-commutativeMonoid)
 
+open import Algebra.Definitions _≈_
+  using (Invertible; LeftInvertible; RightInvertible)
+open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid
+  using (invertibleˡ⇒invertible; invertibleʳ⇒invertible)
 open import Algebra.Properties.Ring ring
-  using (-0#≈0#; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive)
+  using (x-0#≈x; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive)
 open import Relation.Binary.Definitions using (Symmetric)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
-open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid
 
 private variable
   x y z : Carrier
 
 
-open import Algebra.Apartness.Properties.HeytingCommutativeRing heytingCommutativeRing public
-
-invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y
+invertibleˡ⇒# : LeftInvertible 1# _*_ (x - y) → x # y
 invertibleˡ⇒# = invertible⇒# ∘ invertibleˡ⇒invertible
 
-invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y
+invertibleʳ⇒# : RightInvertible 1# _*_ (x - y) → x # y
 invertibleʳ⇒# = invertible⇒# ∘ invertibleʳ⇒invertible
 
 1#0 : 1# # 0#
 1#0 = invertibleˡ⇒# (1# , 1*[x-0]≈x)
   where
   1*[x-0]≈x : 1# * (x - 0#) ≈ x
-  1*[x-0]≈x {x} = trans (*-identityˡ (x - 0#)) (x-0≈x x)
+  1*[x-0]≈x {x} = trans (*-identityˡ (x - 0#)) (x-0#≈x x)
 
 x#0y#0→xy#0 : x # 0# → y # 0# → x * y # 0#
 x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
   where
+  open ≈-Reasoning setoid
 
-  helper : Invertible _≈_ 1# _*_ (x - 0#) → Invertible _≈_ 1# _*_ (y - 0#) → x * y # 0#
+  helper : Invertible 1# _*_ (x - 0#) → Invertible 1# _*_ (y - 0#) → x * y # 0#
   helper (x⁻¹ , x⁻¹*x≈1 , x*x⁻¹≈1) (y⁻¹ , y⁻¹*y≈1 , y*y⁻¹≈1)
     = invertibleˡ⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1)
     where
-    open ≈-Reasoning setoid
 
     y⁻¹*x⁻¹*x*y≈1 : y⁻¹ * x⁻¹ * (x * y - 0#) ≈ 1#
     y⁻¹*x⁻¹*x*y≈1 = begin
-      y⁻¹ * x⁻¹ * (x * y - 0#)     ≈⟨ *-congˡ (x-0≈x (x * y)) ⟩
+      y⁻¹ * x⁻¹ * (x * y - 0#)     ≈⟨ *-congˡ (x-0#≈x (x * y)) ⟩
       y⁻¹ * x⁻¹ * (x * y)          ≈⟨ *-assoc y⁻¹ x⁻¹ (x * y) ⟩
-      y⁻¹ * (x⁻¹ * (x * y))       ≈⟨ *-congˡ (*-assoc x⁻¹ x y) ⟨
-      y⁻¹ * ((x⁻¹ * x) * y)       ≈⟨ *-congˡ (*-congʳ (*-congˡ (x-0≈x x))) ⟨
+      y⁻¹ * (x⁻¹ * (x * y))        ≈⟨ *-congˡ (*-assoc x⁻¹ x y) ⟨
+      y⁻¹ * ((x⁻¹ * x) * y)        ≈⟨ *-congˡ (*-congʳ (*-congˡ (x-0#≈x x))) ⟨
       y⁻¹ * ((x⁻¹ * (x - 0#)) * y) ≈⟨ *-congˡ (*-congʳ x⁻¹*x≈1) ⟩
       y⁻¹ * (1# * y)               ≈⟨ *-congˡ (*-identityˡ y) ⟩
-      y⁻¹ * y                     ≈⟨ *-congˡ (x-0≈x y) ⟨
+      y⁻¹ * y                      ≈⟨ *-congˡ (x-0#≈x y) ⟨
       y⁻¹ * (y - 0#)               ≈⟨ y⁻¹*y≈1 ⟩
-      1# ∎
+      1#                           ∎
 
 #-sym : Symmetric _#_
 #-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1)
   where
   open ≈-Reasoning setoid
-  InvX-Y : Invertible _≈_ 1# _*_ (x - y)
+  InvX-Y : Invertible 1# _*_ (x - y)
   InvX-Y = #⇒invertible x#y
 
   x-y⁻¹ = InvX-Y .proj₁
@@ -82,27 +83,26 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
   x-y⁻¹*y-x≈1 : (- x-y⁻¹) * (y - x) ≈ 1#
   x-y⁻¹*y-x≈1 = begin
     (- x-y⁻¹) * (y - x)   ≈⟨ -‿distribˡ-* x-y⁻¹ (y - x) ⟨
-    - (x-y⁻¹ * (y - x))    ≈⟨ -‿cong (*-congˡ y-x≈-[x-y]) ⟩
+    - (x-y⁻¹ * (y - x))   ≈⟨ -‿cong (*-congˡ y-x≈-[x-y]) ⟩
     - (x-y⁻¹ * - (x - y)) ≈⟨ -‿cong (-‿distribʳ-* x-y⁻¹ (x - y)) ⟨
-    - - (x-y⁻¹ * (x - y))  ≈⟨ -‿involutive (x-y⁻¹ * ((x - y))) ⟩
-    x-y⁻¹ * (x - y)        ≈⟨ InvX-Y .proj₂ .proj₁ ⟩
-    1# ∎
+    - - (x-y⁻¹ * (x - y)) ≈⟨ -‿involutive (x-y⁻¹ * ((x - y))) ⟩
+    x-y⁻¹ * (x - y)       ≈⟨ InvX-Y .proj₂ .proj₁ ⟩
+    1#                    ∎
 
 #-congʳ : x ≈ y → x # z → y # z
-#-congʳ {x} {y} {z} x≈y x#z = helper (#⇒invertible x#z)
+#-congʳ {x} {y} {z} x≈y = helper ∘ #⇒invertible
   where
+  open ≈-Reasoning setoid
 
-  helper : Invertible _≈_ 1# _*_ (x - z) → y # z
+  helper : Invertible 1# _*_ (x - z) → y # z
   helper (x-z⁻¹ , x-z⁻¹*x-z≈1# , x-z*x-z⁻¹≈1#)
     = invertibleˡ⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1)
     where
-    open ≈-Reasoning setoid
-
     x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1#
     x-z⁻¹*y-z≈1 = begin
       x-z⁻¹ * (y - z) ≈⟨ *-congˡ (+-congʳ x≈y) ⟨
-      x-z⁻¹ * (x - z)  ≈⟨ x-z⁻¹*x-z≈1# ⟩
-      1# ∎
+      x-z⁻¹ * (x - z) ≈⟨ x-z⁻¹*x-z≈1# ⟩
+      1#              ∎
 
 #-congˡ : y ≈ z → x # y → x # z
-#-congˡ y≈z x#y = #-sym (#-congʳ y≈z (#-sym x#y))
+#-congˡ y≈z = #-sym ∘ #-congʳ y≈z ∘ #-sym

From 3786f5588db914a4ffc89dd98835e065287e8c9d Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 09:36:16 +0000
Subject: [PATCH 07/14] fix: `CHANGELOG` plus tidying up

---
 CHANGELOG.md                                  | 24 ++++++++++++++++++-
 .../Properties/HeytingCommutativeRing.agda    |  1 +
 .../Apartness/Properties/HeytingField.agda    |  7 +++---
 src/Relation/Binary/Properties/DecSetoid.agda |  5 ++--
 4 files changed, 30 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a0b43bbcb5..84120fb166 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,14 @@ Non-backwards compatible changes
 * The definitions of `Algebra.Structures.IsHeyting*` and
   `Algebra.Structures.IsHeyting*` have been refactored, together
   with that of `Relation.Binary.Definitions.Tight` on which they depend.
+  Specifically:
+  - `Tight _≈_ _#_` has been redefined to drop the redundant
+    second conjunct, because it is equivalent to `Irreflexive _≈_ _#_`.
+  - new definitions: `(Is)TightApartnessRelation` structure/bundle
+  - the definition of `HeytingCommutativeRing` now drops the properties of
+    invertibility, in favour of moving them to `HeytingField`.
+  - both `Heyting*` algebraic structure/bundles have been redefined to base
+    off an underlying `TightApartnessRelation`.
 
 Minor improvements
 ------------------
@@ -144,9 +152,23 @@ Additions to existing modules
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
 
+* In `Algebra.Properties.AbelianGroup`:
+  ```agda
+  x-ε≈x : RightIdentity ε _-_
+  ```
+
+* In `Algebra.Properties.RingWithoutOne`:
+  ```agda
+  x-0#≈x : RightIdentity 0# _-_
+  ```
+
 * In `Relation.Binary.Properties.DecSetoid`:
   ```agda
   ≉-isTightApartnessRelation : IsTightApartnessRelation _≈_ _#_
   ≉-tightApartnessRelation   : TightApartnessRelation _ _ _
   ```
-
+  Additionally,
+  ```agda
+  ≉-tight : Tight _≈_ _≉_
+  ```
+  has been redefined to reflect the change in the definition of `Tight`.
diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
index 0bdec58432..4a0ce9b531 100644
--- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
+++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
@@ -17,6 +17,7 @@ open HeytingCommutativeRing HCR
 open CommutativeRing commutativeRing using (ring)
 open import Algebra.Properties.Ring ring using (x-0#≈x)
 
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Apartness/Properties/HeytingField.agda b/src/Algebra/Apartness/Properties/HeytingField.agda
index b341b12e6e..196e637bd9 100644
--- a/src/Algebra/Apartness/Properties/HeytingField.agda
+++ b/src/Algebra/Apartness/Properties/HeytingField.agda
@@ -27,8 +27,9 @@ open import Algebra.Properties.Ring ring
 open import Relation.Binary.Definitions using (Symmetric)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
-private variable
-  x y z : Carrier
+private
+  variable
+    x y z : Carrier
 
 
 invertibleˡ⇒# : LeftInvertible 1# _*_ (x - y) → x # y
@@ -85,7 +86,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
     (- x-y⁻¹) * (y - x)   ≈⟨ -‿distribˡ-* x-y⁻¹ (y - x) ⟨
     - (x-y⁻¹ * (y - x))   ≈⟨ -‿cong (*-congˡ y-x≈-[x-y]) ⟩
     - (x-y⁻¹ * - (x - y)) ≈⟨ -‿cong (-‿distribʳ-* x-y⁻¹ (x - y)) ⟨
-    - - (x-y⁻¹ * (x - y)) ≈⟨ -‿involutive (x-y⁻¹ * ((x - y))) ⟩
+    - - (x-y⁻¹ * (x - y)) ≈⟨ -‿involutive (x-y⁻¹ * (x - y)) ⟩
     x-y⁻¹ * (x - y)       ≈⟨ InvX-Y .proj₂ .proj₁ ⟩
     1#                    ∎
 
diff --git a/src/Relation/Binary/Properties/DecSetoid.agda b/src/Relation/Binary/Properties/DecSetoid.agda
index 44fd2012e5..888091a80f 100644
--- a/src/Relation/Binary/Properties/DecSetoid.agda
+++ b/src/Relation/Binary/Properties/DecSetoid.agda
@@ -11,18 +11,17 @@ open import Relation.Binary.Bundles
 
 module Relation.Binary.Properties.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where
 
-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; IsTightApartnessRelation; IsDecEquivalence)
+  using (IsApartnessRelation; IsTightApartnessRelation)
 open import Relation.Nullary.Decidable.Core
   using (yes; no; decidable-stable)
 
 open DecSetoid S using (_≈_; _≉_; _≟_; setoid; trans)
-open SetoidProperties setoid
+open SetoidProperties setoid using (≉-sym; ≉-irrefl)
 
 ≉-cotrans : Cotransitive _≉_
 ≉-cotrans {x} {y} x≉y z with x ≟ z | z ≟ y

From 31b51a6d2262626ad5a1d48e1324faf57ded2217 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 09:58:22 +0000
Subject: [PATCH 08/14] refactor: resolve merge of #2576

---
 src/Algebra/Apartness/Structures.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda
index 4ecf66531c..6bc71d835e 100644
--- a/src/Algebra/Apartness/Structures.agda
+++ b/src/Algebra/Apartness/Structures.agda
@@ -32,6 +32,7 @@ record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
 
   open IsCommutativeRing isCommutativeRing public
   open IsTightApartnessRelation isTightApartnessRelation public
+    using (isApartnessRelation; tight)
   open IsApartnessRelation isApartnessRelation public
     renaming
       ( irrefl  to #-irrefl

From f89109357847f3c002cb1eda9dac94c1d37ec85b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 10:16:56 +0000
Subject: [PATCH 09/14] refactor: another attempt to resolve merge of #2576

---
 CHANGELOG.md                                  |  6 +++++
 .../Properties/HeytingCommutativeRing.agda    |  8 ++++++-
 .../Apartness/Properties/HeytingField.agda    | 24 -------------------
 3 files changed, 13 insertions(+), 25 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index faba77f347..e66fa6629a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -42,6 +42,12 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Apartness.Properties.HeytingCommutativeRing`:
+  ```agda
+  x-0≈x  ↦   Algebra.Properties.Ring.x-0#≈x
+  #-sym  ↦   Algebra.Apartness.Structures.IsHeytingCommutativeRing.#-sym
+  ```
+
 * In `Algebra.Definitions.RawMagma`:
   ```agda
   _∣∣_   ↦  _∥_
diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
index 4a0ce9b531..e9d5523839 100644
--- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
+++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
@@ -13,7 +13,7 @@ module Algebra.Apartness.Properties.HeytingCommutativeRing
 
 open import Algebra.Bundles using (CommutativeRing)
 
-open HeytingCommutativeRing HCR
+open HeytingCommutativeRing HCR using (commutativeRing)
 open CommutativeRing commutativeRing using (ring)
 open import Algebra.Properties.Ring ring using (x-0#≈x)
 
@@ -31,3 +31,9 @@ x-0≈x = x-0#≈x
 "Warning: x-0≈x was deprecated in v2.3.
 Please use Algebra.Properties.Ring.x-0#≈x instead."
 #-}
+
+open HeytingCommutativeRing HCR public using (#-sym)
+{-# WARNING_ON_USAGE #-sym
+"Warning: #-sym was deprecated in v2.3.
+Please use Algebra.Apartness.Structures.IsHeytingCommutativeRing.#-sym instead."
+#-}
diff --git a/src/Algebra/Apartness/Properties/HeytingField.agda b/src/Algebra/Apartness/Properties/HeytingField.agda
index 196e637bd9..6cae113896 100644
--- a/src/Algebra/Apartness/Properties/HeytingField.agda
+++ b/src/Algebra/Apartness/Properties/HeytingField.agda
@@ -66,30 +66,6 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
       y⁻¹ * (y - 0#)               ≈⟨ y⁻¹*y≈1 ⟩
       1#                           ∎
 
-#-sym : Symmetric _#_
-#-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1)
-  where
-  open ≈-Reasoning setoid
-  InvX-Y : Invertible 1# _*_ (x - y)
-  InvX-Y = #⇒invertible x#y
-
-  x-y⁻¹ = InvX-Y .proj₁
-
-  y-x≈-[x-y] : y - x ≈ - (x - y)
-  y-x≈-[x-y] = begin
-    y - x     ≈⟨ +-congʳ (-‿involutive y) ⟨
-    - - y - x ≈⟨ -‿anti-homo-+ x (- y) ⟨
-    - (x - y) ∎
-
-  x-y⁻¹*y-x≈1 : (- x-y⁻¹) * (y - x) ≈ 1#
-  x-y⁻¹*y-x≈1 = begin
-    (- x-y⁻¹) * (y - x)   ≈⟨ -‿distribˡ-* x-y⁻¹ (y - x) ⟨
-    - (x-y⁻¹ * (y - x))   ≈⟨ -‿cong (*-congˡ y-x≈-[x-y]) ⟩
-    - (x-y⁻¹ * - (x - y)) ≈⟨ -‿cong (-‿distribʳ-* x-y⁻¹ (x - y)) ⟨
-    - - (x-y⁻¹ * (x - y)) ≈⟨ -‿involutive (x-y⁻¹ * (x - y)) ⟩
-    x-y⁻¹ * (x - y)       ≈⟨ InvX-Y .proj₂ .proj₁ ⟩
-    1#                    ∎
-
 #-congʳ : x ≈ y → x # z → y # z
 #-congʳ {x} {y} {z} x≈y = helper ∘ #⇒invertible
   where

From a8d62848198bdc57609ba59dc947d2a210c9a241 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 10:40:01 +0000
Subject: [PATCH 10/14] refactor: re-export from
 `Relation.Binary.Properties.(Dec)Setoid`

---
 CHANGELOG.md                                  |  7 +++
 .../Rational/Unnormalised/Properties.agda     | 46 ++++++++-----------
 2 files changed, 25 insertions(+), 28 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e66fa6629a..38138c5b91 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -185,6 +185,13 @@ Additions to existing modules
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
 
+* In `Data.Rational.Unnormalised.Properties`:
+  ```agda
+  ≄-apartnessRelation        : ApartnessRelation _ _ _
+  ≄-isTightApartnessRelation : IsTightApartnessRelation _≃_ _≄_
+  ≄-tightApartnessRelation   : TightApartnessRelation _ _ _
+  ```
+
 * In `Relation.Binary.Properties.DecSetoid`:
   ```agda
   ≉-isTightApartnessRelation : IsTightApartnessRelation _≈_ _#_
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index cf4c461fec..b1ba874008 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -40,6 +40,8 @@ open import Relation.Binary.Definitions
   using (Reflexive; Symmetric; Transitive; Cotransitive; Tight; Decidable; Antisymmetric; Asymmetric; Dense; Total; Trans; Trichotomous; Irreflexive; Irrelevant; _Respectsˡ_; _Respectsʳ_; _Respects₂_; tri≈; tri<; tri>)
 import Relation.Binary.Consequences as BC
 open import Relation.Binary.PropositionalEquality
+import Relation.Binary.Properties.Setoid as SetoidProperties
+import Relation.Binary.Properties.DecSetoid as DecSetoidProperties
 import Relation.Binary.Properties.Poset as PosetProperties
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Relation.Binary.Reasoning.Syntax
@@ -106,18 +108,6 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* 
 0≄1 : 0ℚᵘ ≄ 1ℚᵘ
 0≄1 = Dec.from-no (0ℚᵘ ≃? 1ℚᵘ)
 
-≃-≄-irreflexive : Irreflexive _≃_ _≄_
-≃-≄-irreflexive x≃y x≄y = x≄y x≃y
-
-≄-symmetric : Symmetric _≄_
-≄-symmetric x≄y y≃x = x≄y (≃-sym y≃x)
-
-≄-cotransitive : Cotransitive _≄_
-≄-cotransitive {x} {y} x≄y z with x ≃? z | z ≃? y
-... | no  x≄z | _       = inj₁ x≄z
-... | yes _   | no z≄y  = inj₂ z≄y
-... | yes x≃z | yes z≃y = contradiction (≃-trans x≃z z≃y) x≄y
-
 ≃-isEquivalence : IsEquivalence _≃_
 ≃-isEquivalence = record
   { refl  = ≃-refl
@@ -131,22 +121,6 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* 
   ; _≟_           = _≃?_
   }
 
-≄-isApartnessRelation : IsApartnessRelation _≃_ _≄_
-≄-isApartnessRelation = record
-  { irrefl  = ≃-≄-irreflexive
-  ; sym     = ≄-symmetric
-  ; cotrans = ≄-cotransitive
-  }
-
-≄-tight : Tight _≃_ _≄_
-≄-tight p q = Dec.decidable-stable (p ≃? q)
-
-≄-isTightApartnessRelation : IsTightApartnessRelation _≃_ _≄_
-≄-isTightApartnessRelation = record
-  { isApartnessRelation = ≄-isApartnessRelation
-  ; tight = ≄-tight
-  }
-
 ≃-setoid : Setoid 0ℓ 0ℓ
 ≃-setoid = record
   { isEquivalence = ≃-isEquivalence
@@ -157,6 +131,22 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* 
   { isDecEquivalence = ≃-isDecEquivalence
   }
 
+open SetoidProperties ≃-setoid public
+  renaming
+  ( ≉-sym to ≄-symmetric
+  ; ≉-irrefl to ≃-≄-irreflexive
+  )
+
+open DecSetoidProperties ≃-decSetoid public
+  renaming
+  ( ≉-cotrans to ≄-cotransitive
+  ; ≉-tight to ≄-tight
+  ; ≉-isApartnessRelation to ≄-isApartnessRelation
+  ; ≉-apartnessRelation to ≄-ApartnessRelation
+  ; ≉-isTightApartnessRelation to ≄-isTightApartnessRelation
+  ; ≉-tightApartnessRelation to ≄-tightApartnessRelation
+  )
+
 module ≃-Reasoning = ≈-Reasoning ≃-setoid
 
 ↥p≡0⇒p≃0 : ∀ p → ↥ p ≡ 0ℤ → p ≃ 0ℚᵘ

From 1f9a4c18d75f8889ac1bdb6310fd219d1776354c Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 10:46:03 +0000
Subject: [PATCH 11/14] refactor: tighten re-export from
 `Relation.Binary.Properties.DecSetoid`

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

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index ab739053e1..cdc5edf3dc 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -1279,7 +1279,7 @@ module _ where
     using (+-group; zeroˡ; *-congʳ; isCommutativeRing)
 
   open GroupProperties +-group
-  open DecSetoidProperties ≡-decSetoid
+  open DecSetoidProperties ≡-decSetoid using (≉-isTightApartnessRelation)
 
   #⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q)
   #⇒invertible {p} {q} p≢q = let r = p - q in 1/ r , *-inverseˡ r , *-inverseʳ r

From 48bef4a1e7ade3f84bd32f3e480fc8320af40246 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 11:03:11 +0000
Subject: [PATCH 12/14] refactor: re-export from `apartnessRelation` from
 `HeytingCommutativeRing`

---
 CHANGELOG.md                       | 4 ++--
 src/Algebra/Apartness/Bundles.agda | 3 +++
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 38138c5b91..496e6090f9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -123,12 +123,12 @@ New modules
 Additions to existing modules
 -----------------------------
 
-* In `Algebra.Apartness.Bundles`:
+* In `Algebra.Apartness.Bundles.HeytingCommutativeRing`:
   ```agda
   TightApartnessRelation c ℓ₁ ℓ₂ : Set _
   ```
 
-* In `Algebra.Apartness.Structures`:
+* In `Algebra.Apartness.Structures.IsHeytingCommutativeRing`:
   ```agda
   IsTightApartnessRelation _≈_ _#_ : Set _
   ```
diff --git a/src/Algebra/Apartness/Bundles.agda b/src/Algebra/Apartness/Bundles.agda
index ff6768b873..489f8c819f 100644
--- a/src/Algebra/Apartness/Bundles.agda
+++ b/src/Algebra/Apartness/Bundles.agda
@@ -39,6 +39,9 @@ record HeytingCommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ
   tightApartnessRelation : TightApartnessRelation c ℓ₁ ℓ₂
   tightApartnessRelation = record { isTightApartnessRelation = isTightApartnessRelation }
 
+  open TightApartnessRelation tightApartnessRelation public
+    using (apartnessRelation)
+
 
 record HeytingField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix  8 -_

From cdc57d2eafac695a4b708ba686bc0a291ae167df Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 11:11:39 +0000
Subject: [PATCH 13/14] fix: better `CHANGELOG`?

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 496e6090f9..507e4956d8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,7 +10,7 @@ Bug-fixes
 ---------
 
 * In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation`
-  to `#-sym` in order to avoid overloaded projection.
+  to `#-sym` in order to avoid overloaded projection. The field names
   `irrefl` and `cotrans` are similarly renamed for the sake of consistency.
 
 Non-backwards compatible changes
@@ -25,9 +25,11 @@ Non-backwards compatible changes
   `Algebra.Structures.IsHeyting*` have been refactored, together
   with that of `Relation.Binary.Definitions.Tight` on which they depend.
   Specifically:
-  - `Tight _≈_ _#_` has been redefined to drop the redundant
-    second conjunct, because it is equivalent to `Irreflexive _≈_ _#_`.
-  - new definitions: `(Is)TightApartnessRelation` structure/bundle
+  - `Tight _≈_ _#_` has been redefined as `∀ x y → ¬ x # y → x ≈ y`,
+    dropping the redundant second conjunct, because it is equivalent to
+    `Irreflexive _≈_ _#_`.
+  - new definitions: `(Is)TightApartnessRelation` structure/bundle, exploiting
+    the above redefinition.
   - the definition of `HeytingCommutativeRing` now drops the properties of
     invertibility, in favour of moving them to `HeytingField`.
   - both `Heyting*` algebraic structure/bundles have been redefined to base

From fb2da3e85cf01963367de58d1f2e051a4a51f1b0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 11:14:48 +0000
Subject: [PATCH 14/14] fix: one last re-export?

---
 src/Algebra/Apartness/Bundles.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Apartness/Bundles.agda b/src/Algebra/Apartness/Bundles.agda
index 489f8c819f..a6a4addcdd 100644
--- a/src/Algebra/Apartness/Bundles.agda
+++ b/src/Algebra/Apartness/Bundles.agda
@@ -65,4 +65,4 @@ record HeytingField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   heytingCommutativeRing = record { isHeytingCommutativeRing = isHeytingCommutativeRing }
 
   open HeytingCommutativeRing heytingCommutativeRing public
-    using (commutativeRing; tightApartnessRelation)
+    using (commutativeRing; tightApartnessRelation; apartnessRelation)