diff --git a/CHANGELOG.md b/CHANGELOG.md
index 151d86902b..a0f47fec40 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -50,6 +50,10 @@ Highlights
 Bug-fixes
 ---------
 
+* In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation`
+  to `#-sym` in order to avoid overloaded projection. The field names
+  `irrefl` and `cotrans` are similarly renamed for the sake of consistency.
+
 * Removed unnecessary parameter `zero : Zero 0# *` from
   `Algebra.Structures.IsNonAssociativeRing`.
 
@@ -72,6 +76,21 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* The definitions of `Algebra.Structures.IsHeyting*` and
+  `Algebra.Bundles.Heyting*` have been refactored, together
+  with that of `Relation.Binary.Definitions.Tight` on which they depend.
+  Specifically:
+  - `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
+    off an underlying `TightApartnessRelation`.
+  - both also further require `_+_`/`_*_` to be `StronglyExtensional` wrt `_#_`.
+
 * A major overhaul of the `Function` hierarchy sees the systematic development
   and use of the theory of the left inverse `from` to a given `Surjective` function
   `to`, as a consequence of which we can achieve full symmetry of `Bijection`, in
@@ -177,6 +196,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`:
   ```agda
   StarLeftExpansive     ↦  Relation.Binary.Definitions.KleeneAlgebra.StarLeftExpansive
@@ -277,6 +302,15 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Apartness.Consequences`, relationships between definitions, given
+  properties of a given apartness relation, notably `Cotransitive _#_`.
+
+* `Algebra.Apartness.Definitions`, properties of algebraic operations wrt
+  a given apartness relation `_#_`.
+
+* `Algebra.Apartness.Properties.HeytingField`, refactoring the existing
+  `Algebra.Apartness.Properties.HeytingCommutativeRing`.
+
 * `Algebra.Properties.KleeneAlgebra` has been completely rewritten.
 
 * `Codata.Guarded.Stream.Relation.Unary.Linked` for a proof that each pair
@@ -317,6 +351,18 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Apartness.Bundles.HeytingCommutativeRing`:
+  ```agda
+  TightApartnessRelation c ℓ₁ ℓ₂ : Set _
+  ```
+
+* In `Algebra.Apartness.Structures.IsHeytingCommutativeRing`:
+  ```agda
+  IsTightApartnessRelation _≈_ _#_ : Set _
+  +-stronglyExtensional : StronglyExtensional _#_ _+_
+  *-stronglyExtensional : StronglyExtensional _#_ _*_
+  ```
+
 * In `Algebra.Consequences.Base`:
   ```agda
   almost⇒exceptˡ : _AlmostLeftCancellative′_ _≈_ P _•_ →
@@ -347,6 +393,21 @@ Additions to existing modules
   Except_RightCancellative_    : (P : Pred A p) → Op₂ A → Set _
   ```
 
+* In `Algebra.Properties.AbelianGroup`:
+  ```agda
+  x-ε≈x : RightIdentity ε _-_
+  ```
+
+* In `Algebra.Properties.RingWithoutOne`:
+  ```agda
+  x-0#≈x : RightIdentity 0# _-_
+  ```
+
+* In `Algebra.Structures.IsKleeneAlgebra`:
+  ```agda
+  _≤_            : Rel A _
+  ```
+
 * In `Algebra.Properties.KleeneAlgebra`:
   ```agda
   ≤-reflexive    : _≈_ ⇒ _≤_
@@ -359,11 +420,6 @@ Additions to existing modules
   poset          : Poset _ _
   ```
 
-* In `Algebra.Structures.IsKleeneAlgebra`:
-  ```agda
-  _≤_            : Rel A _
-  ```
-
 * In `Data.Bool.Properties`:
   ```agda
   ∨-monoid : Monoid 0ℓ 0ℓ
@@ -478,6 +534,29 @@ Additions to existing modules
                 (q ℤ.* + p) / (r ℕ.* p) ≡ q / r
   i/n+j/n≡[i+j]/n : ∀ (i j : ℤ) (n : ℕ) .{{_ : ℕ.NonZero n }} →
                     i / n + j / n ≡ (i ℤ.+ j) / n
+  +-stronglyCongruentˡ  : ∀ p → StronglyCongruent₁ _≢_ (p +_)
+  +-stronglyCongruentʳ  : ∀ r → StronglyCongruent₁ _≢_ (_+ r)
+  +-stronglyCongruent   : StronglyCongruent₂ _≢_ _+_
+  +-stronglyExtensional : StronglyExtensional _≢_ _+_
+  *-stronglyCongruentˡ  : ∀ p → StronglyCongruent₁ _≢_ (p *_)
+  *-stronglyCongruentʳ  : ∀ r → StronglyCongruent₁ _≢_ (_* r)
+  *-stronglyCongruent   : StronglyCongruent₂ _≢_ _*_
+  *-stronglyExtensional : StronglyExtensional _≢_ _*_
+  ```
+
+* In `Data.Rational.Unnormalised.Properties`:
+  ```agda
+  ≄-apartnessRelation        : ApartnessRelation _ _ _
+  ≄-isTightApartnessRelation : IsTightApartnessRelation _≃_ _≄_
+  ≄-tightApartnessRelation   : TightApartnessRelation _ _ _
+  +-stronglyCongruentˡ  : ∀ p → StronglyCongruent₁ _≄_ (p +_)
+  +-stronglyCongruentʳ  : ∀ r → StronglyCongruent₁ _≄_ (_+ r)
+  +-stronglyCongruent   : StronglyCongruent₂ _≄_ _+_
+  +-stronglyExtensional : StronglyExtensional _≄_ _+_
+  *-stronglyCongruentˡ  : ∀ p → StronglyCongruent₁ _≄_ (p *_)
+  *-stronglyCongruentʳ  : ∀ r → StronglyCongruent₁ _≄_ (_* r)
+  *-stronglyCongruent   : StronglyCongruent₂ _≄_ _*_
+  *-stronglyExtensional : StronglyExtensional _≄_ _*_
   ```
 
 * In `Data.Vec.Properties`:
@@ -596,6 +675,7 @@ Additions to existing modules
 
   HalfRightAdjoint : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → (B → A) → Set _
   HalfRightAdjoint _≤_ _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y)
+
   module KleeneAlgebra (_≤_ : Rel A ℓ₁) where
     StarLeftExpansive     : ∀ (e : A) (_+_ _*_ : Fun₂ A) (_⋆ : Fun₁ A) → Set _
     StarRightExpansive    : ∀ (e : A) (_+_ _*_ : Fun₂ A) (_⋆ : Fun₁ A) → Set _
@@ -605,6 +685,17 @@ Additions to existing modules
     StarDestructive       : ∀ (_+_ _*_ : Fun₂ A) (_⋆ : Fun₁ A) → Set _
   ```
 
+* 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`.
+
 * In `Relation.Unary`:
   ```agda
   Unique         : Rel A ℓ₁ → Pred A ℓ₂ → Pred A _
diff --git a/src/Algebra/Apartness/Bundles.agda b/src/Algebra/Apartness/Bundles.agda
index 1bf6ddca13..719e8eb5c3 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 using (IsHeytingCommutativeRing; IsHeytingField)
@@ -36,8 +36,11 @@ 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 }
+
+  open TightApartnessRelation tightApartnessRelation public
+    using (apartnessRelation)
 
 
 record HeytingField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -61,5 +64,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; apartnessRelation)
diff --git a/src/Algebra/Apartness/Consequences.agda b/src/Algebra/Apartness/Consequences.agda
new file mode 100644
index 0000000000..816f01ab9d
--- /dev/null
+++ b/src/Algebra/Apartness/Consequences.agda
@@ -0,0 +1,36 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Lemmas relating algebraic definitions wrt an apartness.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core using (Rel)
+
+module Algebra.Apartness.Consequences
+  {a ℓ} {A : Set a} (_#_ : Rel A ℓ) where
+
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Apartness.Definitions _#_
+open import Data.Product.Base using (_,_)
+import Data.Sum.Base as Sum
+open import Level using (Level)
+open import Relation.Binary.Definitions
+  using (Cotransitive)
+
+private
+  variable
+    r : Level
+    f : Op₁ A
+    _∙_ : Op₂ A
+
+
+------------------------------------------------------------------------
+-- Cotransitive plus StronglyCongruent₂ implies StronglyExtensional
+
+cotransitive∧congruent⇒extensional : Cotransitive _#_ →
+  StronglyCongruent₂ _∙_ → StronglyExtensional _∙_
+cotransitive∧congruent⇒extensional
+  {_∙_ = _∙_} cotrans cong@(congˡ , congʳ) {y = y} {w = w} xy#wz
+  = Sum.map (congʳ y) (congˡ w) (cotrans xy#wz (w ∙ y))
diff --git a/src/Algebra/Apartness/Definitions.agda b/src/Algebra/Apartness/Definitions.agda
new file mode 100644
index 0000000000..a48778d219
--- /dev/null
+++ b/src/Algebra/Apartness/Definitions.agda
@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of operations, relative to an apartness relation
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core using (Rel; _⇒_)
+
+module Algebra.Apartness.Definitions
+  {a ℓ} {A : Set a}   -- The underlying set
+  (_#_ : Rel A ℓ)     -- The underlying apartness
+  where
+
+open import Algebra.Core using (Op₁; Op₂)
+open import Data.Product.Base using (_×_)
+open import Data.Sum.Base using (_⊎_)
+open import Function.Base using (_on_)
+
+
+------------------------------------------------------------------------
+-- Properties of operations
+
+module _ (f : Op₁ A) where
+
+  StronglyCongruent₁  : Set _
+  StronglyCongruent₁  = (_#_ on f) ⇒ _#_
+
+module _ (_∙_ : Op₂ A) where
+
+  StronglyCongruent₂ : Set _
+  StronglyCongruent₂ =
+    (∀ x → StronglyCongruent₁ (x ∙_)) × (∀ z → StronglyCongruent₁ (_∙ z))
+
+  StronglyExtensional : Set _
+  StronglyExtensional = ∀ {x y w z} → (x ∙ y) # (w ∙ z) → x # w ⊎ y # z
+
diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
index 5ee3da4273..5bf97ca6ce 100644
--- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
+++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
@@ -9,76 +9,31 @@
 open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
 
 module Algebra.Apartness.Properties.HeytingCommutativeRing
-  {c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where
+  {c ℓ₁ ℓ₂} (heytingCommutativeRing : 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.Bundles using (CommutativeRing)
 
-open HeytingCommutativeRing HCR
-open CommutativeRing commutativeRing using (ring; *-commutativeMonoid)
+open HeytingCommutativeRing heytingCommutativeRing using (commutativeRing)
+open CommutativeRing commutativeRing using (ring)
+open import Algebra.Properties.Ring ring using (x-0#≈x)
 
-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
-
-invertibleˡ⇒# : LeftInvertible _≈_ 1# _*_ (x - y) → x # y
-invertibleˡ⇒# = invertible⇒# ∘ invertibleˡ⇒invertible
-
-invertibleʳ⇒# : RightInvertible _≈_ 1# _*_ (x - y) → x # y
-invertibleʳ⇒# = invertible⇒# ∘ invertibleʳ⇒invertible
-
-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# ∎
-
-#-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))
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 3.0
+
+x-0≈x = x-0#≈x
+{-# WARNING_ON_USAGE x-0≈x
+"Warning: x-0≈x was deprecated in v3.0.
+Please use Algebra.Properties.Ring.x-0#≈x instead."
+#-}
+
+open HeytingCommutativeRing heytingCommutativeRing public using (#-sym)
+{-# WARNING_ON_USAGE #-sym
+"Warning: #-sym was deprecated in v3.0.
+Please use Algebra.Apartness.Structures.IsHeytingCommutativeRing.#-sym instead."
+#-}
diff --git a/src/Algebra/Apartness/Properties/HeytingField.agda b/src/Algebra/Apartness/Properties/HeytingField.agda
new file mode 100644
index 0000000000..1650749e55
--- /dev/null
+++ b/src/Algebra/Apartness/Properties/HeytingField.agda
@@ -0,0 +1,85 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of Heyting Fields
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Apartness.Bundles using (HeytingField)
+
+module Algebra.Apartness.Properties.HeytingField
+  {c ℓ₁ ℓ₂} (heytingField : HeytingField c ℓ₁ ℓ₂) where
+
+open import Function.Base using (_∘_)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Algebra.Bundles using (CommutativeRing)
+
+open HeytingField heytingField
+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 (x-0#≈x; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive)
+open import Relation.Binary.Definitions using (Symmetric)
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+
+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
+
+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
+  open ≈-Reasoning setoid
+
+  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
+
+    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#                           ∎
+
+#-congʳ : x ≈ y → x # z → y # z
+#-congʳ {x} {y} {z} x≈y = helper ∘ #⇒invertible
+  where
+  open ≈-Reasoning setoid
+
+  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
+    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 = #-sym ∘ #-congʳ y≈z ∘ #-sym
diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda
index c11a42346f..fc66fce47f 100644
--- a/src/Algebra/Apartness/Structures.agda
+++ b/src/Algebra/Apartness/Structures.agda
@@ -2,6 +2,8 @@
 -- The Agda standard library
 --
 -- Algebraic structures with an apartness relation
+-- Axiomatisation follows Troelstra and van Dalen,
+-- "Constructivity in Mathematics, Vol. II"
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
@@ -16,23 +18,27 @@ module Algebra.Apartness.Structures
   (_+_ _*_ : Op₂ Carrier) (-_ : Op₁ Carrier) (0# 1# : Carrier)
   where
 
-open import Level using (_⊔_; suc)
-open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₂)
+open import Algebra.Apartness.Definitions _#_ using (StronglyExtensional)
 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 (¬_)
-import Relation.Binary.Properties.ApartnessRelation as AR
+open import Data.Product.Base using (proj₁; proj₂)
+open import Level using (_⊔_; suc)
+open import Relation.Binary.Structures
+  using (IsEquivalence; IsApartnessRelation; IsTightApartnessRelation)
+import Relation.Binary.Properties.ApartnessRelation as Apartness
 
 
 record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
 
   field
-    isCommutativeRing   : IsCommutativeRing _+_ _*_ -_ 0# 1#
-    isApartnessRelation : IsApartnessRelation _≈_ _#_
+    isCommutativeRing        : IsCommutativeRing _+_ _*_ -_ 0# 1#
+    isTightApartnessRelation : IsTightApartnessRelation _≈_ _#_
+    +-stronglyExtensional    : StronglyExtensional _+_
+    *-stronglyExtensional    : StronglyExtensional _*_
 
   open IsCommutativeRing isCommutativeRing public
+  open IsTightApartnessRelation isTightApartnessRelation public
+    using (isApartnessRelation; tight)
   open IsApartnessRelation isApartnessRelation public
     renaming
       ( irrefl  to #-irrefl
@@ -40,18 +46,18 @@ record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
       ; cotrans to #-cotrans
       )
 
-  field
-    #⇒invertible : ∀ {x y} → x # y → Invertible 1# _*_ (x - y)
-    invertible⇒# : ∀ {x y} → Invertible 1# _*_ (x - y) → x # y
-
   ¬#-isEquivalence : IsEquivalence _¬#_
-  ¬#-isEquivalence = AR.¬#-isEquivalence refl isApartnessRelation
+  ¬#-isEquivalence = Apartness.¬#-isEquivalence refl isApartnessRelation
 
 
 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/Algebra/Properties/AbelianGroup.agda b/src/Algebra/Properties/AbelianGroup.agda
index a488011033..4cd99b773f 100644
--- a/src/Algebra/Properties/AbelianGroup.agda
+++ b/src/Algebra/Properties/AbelianGroup.agda
@@ -11,9 +11,9 @@ open import Algebra.Bundles using (AbelianGroup)
 module Algebra.Properties.AbelianGroup
   {a ℓ} (G : AbelianGroup a ℓ) where
 
-open import Function.Base using (_$_)
-
 open AbelianGroup G
+open import Algebra.Definitions _≈_ using (RightIdentity)
+open import Function.Base using (_$_)
 open import Relation.Binary.Reasoning.Setoid setoid
 
 ------------------------------------------------------------------------
@@ -40,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 3fc141973d..d81dfcfe35 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
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index cdd1ac8bf1..f7475f9f3d 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -9,6 +9,8 @@
 
 module Data.Rational.Properties where
 
+open import Algebra.Apartness.Consequences
+open import Algebra.Apartness.Definitions
 open import Algebra.Apartness
   using (IsHeytingCommutativeRing; IsHeytingField
         ; HeytingCommutativeRing; HeytingField)
@@ -66,7 +68,8 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Relation.Binary.Reasoning.Syntax using (module ≃-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.Nullary.Negation.Core
+  using (¬_; contradiction; contraposition)
 
 open import Algebra.Definitions {A = ℚ} _≡_
 open import Algebra.Structures  {A = ℚ} _≡_
@@ -1354,17 +1357,46 @@ p*q≢0⇒q≢0 {p} {q} pq≢0 q≡0 = pq≢0 $ begin
 
 module _ where
   open CommutativeRing +-*-commutativeRing
-    using (+-group; zeroˡ; *-congʳ; isCommutativeRing)
+    using (+-group; zeroˡ; +-congˡ; +-congʳ; *-congˡ; *-congʳ; isCommutativeRing)
 
   open GroupProperties +-group
   open DecSetoidProperties ≡-decSetoid
+    using (≉-isTightApartnessRelation)
+    renaming (≉-cotrans to ≢-cotransitive)
+
+  -- NB *section* (p +_) clashes with ℤ.+_!!!
+  +-stronglyCongruentˡ : ∀ p → StronglyCongruent₁ _≢_ λ # → p + #
+  +-stronglyCongruentˡ p = contraposition (+-congˡ {x = p})
+
+  +-stronglyCongruentʳ : ∀ r → StronglyCongruent₁ _≢_ (_+ r)
+  +-stronglyCongruentʳ r = contraposition (+-congʳ {x = r})
+
+  +-stronglyCongruent : StronglyCongruent₂ _≢_ _+_
+  +-stronglyCongruent = +-stronglyCongruentˡ , +-stronglyCongruentʳ
+
+  +-stronglyExtensional : StronglyExtensional _≢_ _+_
+  +-stronglyExtensional =
+    cotransitive∧congruent⇒extensional _≢_ ≢-cotransitive +-stronglyCongruent
+
+  *-stronglyCongruentˡ : ∀ p → StronglyCongruent₁ _≢_ (p *_)
+  *-stronglyCongruentˡ p = contraposition (*-congˡ {x = p})
+
+  *-stronglyCongruentʳ : ∀ r → StronglyCongruent₁ _≢_ (_* r)
+  *-stronglyCongruentʳ r = contraposition (*-congʳ {x = r})
+
+  *-stronglyCongruent : StronglyCongruent₂ _≢_ _*_
+  *-stronglyCongruent = *-stronglyCongruentˡ , *-stronglyCongruentʳ
+
+  *-stronglyExtensional : StronglyExtensional _≢_ _*_
+  *-stronglyExtensional =
+    cotransitive∧congruent⇒extensional _≢_ ≢-cotransitive *-stronglyCongruent
 
   #⇒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 = contradiction 1≡0 1≢0
+  invertible⇒# {p} {q} (1/[p-q] , _ , [p-q]/[p-q]≡1) p≡q = 1≢0 1≡0
     where
     open ≈-Reasoning ≡-setoid
     1≡0 : 1ℚ ≡ 0ℚ
@@ -1377,15 +1409,16 @@ module _ where
   isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
   isHeytingCommutativeRing = record
     { isCommutativeRing = isCommutativeRing
-    ; isApartnessRelation = ≉-isApartnessRelation
-    ; #⇒invertible = #⇒invertible
-    ; invertible⇒# = invertible⇒#
+    ; isTightApartnessRelation = ≉-isTightApartnessRelation
+    ; +-stronglyExtensional = +-stronglyExtensional
+    ; *-stronglyExtensional = *-stronglyExtensional
     }
 
   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 0660b45f5a..54a1262348 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -9,15 +9,17 @@
 
 module Data.Rational.Unnormalised.Properties where
 
-open import Algebra.Definitions
-open import Algebra.Structures
-  using (IsMagma; IsSemigroup; IsBand; IsSelectiveMagma
-        ; IsMonoid; IsCommutativeMonoid; IsGroup; IsAbelianGroup
-        ; IsRing; IsCommutativeRing)
-open import Algebra.Bundles
+open import Algebra.Apartness.Consequences
+open import Algebra.Apartness.Definitions
 open import Algebra.Apartness
   using (IsHeytingCommutativeRing; IsHeytingField
         ; HeytingCommutativeRing; HeytingField)
+open import Algebra.Bundles
+open import Algebra.Definitions
+open import Algebra.Structures
+  using (IsMagma; IsSemigroup; IsBand; IsSelectiveMagma; IsMonoid
+        ; IsCommutativeMonoid; IsGroup; IsAbelianGroup; IsRing
+        ; IsCommutativeRing)
 open import Algebra.Lattice
   using (IsSemilattice; IsLattice; IsDistributiveLattice
         ; RawLattice; Semilattice; Lattice; DistributiveLattice)
@@ -42,22 +44,25 @@ import Data.Sign as Sign
 open import Function.Base using (_on_; _$_; _∘_; flip)
 open import Level using (0ℓ)
 open import Relation.Nullary.Decidable.Core as Dec using (yes; no)
-open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Negation.Core
+  using (¬_; contradiction; contraposition)
 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
+  using (IsEquivalence; IsDecEquivalence; IsApartnessRelation; IsTightApartnessRelation
+        ; IsPreorder; IsTotalPreorder; 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>; Monotonic₁; LeftMonotonic; RightMonotonic; Monotonic₂)
-import Relation.Binary.Consequences as BC
+import Relation.Binary.Consequences as Binary
 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
@@ -125,18 +130,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
@@ -150,17 +143,6 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≡? ↥ q ℤ.* 
   ; _≈?_          = _≃?_
   }
 
-≄-isApartnessRelation : IsApartnessRelation _≃_ _≄_
-≄-isApartnessRelation = record
-  { irrefl  = ≃-≄-irreflexive
-  ; sym     = ≄-symmetric
-  ; cotrans = ≄-cotransitive
-  }
-
-≄-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
-
 ≃-setoid : Setoid 0ℓ 0ℓ
 ≃-setoid = record
   { isEquivalence = ≃-isEquivalence
@@ -171,6 +153,22 @@ proj₂ (≄-tight p q) p≃q p≄q = p≄q p≃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ℚᵘ
@@ -391,10 +389,10 @@ _≥?_ = flip _≤?_
 -- Other properties of _≤_
 
 mono⇒cong : ∀ {f} → Monotonic₁ _≤_ _≤_ f → Congruent₁ _≃_ f
-mono⇒cong = BC.mono⇒cong _≃_ _≃_ ≃-sym ≤-reflexive ≤-antisym
+mono⇒cong = Binary.mono⇒cong _≃_ _≃_ ≃-sym ≤-reflexive ≤-antisym
 
 antimono⇒cong : ∀ {f} → Monotonic₁ _≤_ _≥_ f → Congruent₁ _≃_ f
-antimono⇒cong = BC.antimono⇒cong _≃_ _≃_ ≃-sym ≤-reflexive ≤-antisym
+antimono⇒cong = Binary.antimono⇒cong _≃_ _≃_ ≃-sym ≤-reflexive ≤-antisym
 
 ------------------------------------------------------------------------
 -- Properties of _≤ᵇ_
@@ -827,6 +825,21 @@ neg⇒nonZero (mkℚᵘ (-[1+ _ ]) _) = _
 p+p≃0⇒p≃0 : ∀ p → p + p ≃ 0ℚᵘ → p ≃ 0ℚᵘ
 p+p≃0⇒p≃0 (mkℚᵘ ℤ.+0 _) (*≡* _) = *≡* refl
 
+-- Apartness
+
++-stronglyCongruentˡ : ∀ p → StronglyCongruent₁ _≄_ (p +_)
++-stronglyCongruentˡ p = contraposition (+-congʳ p)
+
++-stronglyCongruentʳ : ∀ r → StronglyCongruent₁ _≄_ (_+ r)
++-stronglyCongruentʳ r = contraposition (+-congˡ r)
+
++-stronglyCongruent : StronglyCongruent₂ _≄_ _+_
++-stronglyCongruent = +-stronglyCongruentˡ , +-stronglyCongruentʳ
+
++-stronglyExtensional : StronglyExtensional _≄_ _+_
++-stronglyExtensional =
+  cotransitive∧congruent⇒extensional _≄_ ≄-cotransitive +-stronglyCongruent
+
 ------------------------------------------------------------------------
 -- Properties of _+_ and -_
 
@@ -875,7 +888,7 @@ private
 
 +-mono-≤ : Monotonic₂ _≤_ _≤_ _≤_ _+_
 +-mono-≤ =
-  BC.monoˡ∧monoʳ⇒mono₂ _≤_ _≤_ _≤_ ≤-trans +-monoʳ-≤ +-monoˡ-≤
+  Binary.monoˡ∧monoʳ⇒mono₂ _≤_ _≤_ _≤_ ≤-trans +-monoʳ-≤ +-monoˡ-≤
 
 p≤q⇒p≤r+q : ∀ r .{{_ : NonNegative r}} → p ≤ q → p ≤ r + q
 p≤q⇒p≤r+q {p} {q} r p≤q = subst (_≤ r + q) (+-identityˡ-≡ p) (+-mono-≤ (nonNegative⁻¹ r) p≤q)
@@ -1225,6 +1238,21 @@ p*q≢0⇒q≢0 {p} {q} pq≄0 q≃0 = pq≄0 $ begin-equality
   0ℚᵘ     ∎
   where open ≤-Reasoning
 
+-- Apartness
+
+*-stronglyCongruentˡ : ∀ p → StronglyCongruent₁ _≄_ (p *_)
+*-stronglyCongruentˡ p = contraposition (*-congˡ {x = p})
+
+*-stronglyCongruentʳ : ∀ r → StronglyCongruent₁ _≄_ (_* r)
+*-stronglyCongruentʳ r = contraposition (*-congʳ {x = r})
+
+*-stronglyCongruent : StronglyCongruent₂ _≄_ _*_
+*-stronglyCongruent = *-stronglyCongruentˡ , *-stronglyCongruentʳ
+
+*-stronglyExtensional : StronglyExtensional _≄_ _*_
+*-stronglyExtensional =
+  cotransitive∧congruent⇒extensional _≄_ ≄-cotransitive *-stronglyCongruent
+
 ------------------------------------------------------------------------
 -- Properties of _*_ and -_
 
@@ -1448,15 +1476,16 @@ nonNeg*nonNeg⇒nonNeg p q = nonNegative
 +-*-isHeytingCommutativeRing : IsHeytingCommutativeRing _≃_ _≄_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
 +-*-isHeytingCommutativeRing = record
   { isCommutativeRing   = +-*-isCommutativeRing
-  ; isApartnessRelation = ≄-isApartnessRelation
-  ; #⇒invertible        = ≄⇒invertible
-  ; invertible⇒#        = invertible⇒≄
+  ; isTightApartnessRelation = ≄-isTightApartnessRelation
+  ; +-stronglyExtensional = +-stronglyExtensional
+  ; *-stronglyExtensional = *-stronglyExtensional
   }
 
 +-*-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 9d1ff33219..bf9ac117e6 100644
--- a/src/Relation/Binary/Bundles.agda
+++ b/src/Relation/Binary/Bundles.agda
@@ -413,3 +413,19 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
   open RawRelation rawRelation public
     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 30f32b679d..f45a87e468 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 ed419ebf7a..2d647e5739 100644
--- a/src/Relation/Binary/Properties/DecSetoid.agda
+++ b/src/Relation/Binary/Properties/DecSetoid.agda
@@ -6,22 +6,22 @@
 
 {-# OPTIONS --without-K --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
 
-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)
+  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
@@ -36,8 +36,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) , ≉-irrefl
+≉-tightApartnessRelation : TightApartnessRelation c ℓ ℓ
+≉-tightApartnessRelation = record
+  { isTightApartnessRelation = ≉-isTightApartnessRelation }
+
diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda
index 733ee34b00..84619f1024 100644
--- a/src/Relation/Binary/Structures.agda
+++ b/src/Relation/Binary/Structures.agda
@@ -344,5 +344,12 @@ record IsApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) whe
     sym     : Symmetric _#_
     cotrans : Cotransitive _#_
 
-  _¬#_ : A → A → Set _
+  _¬#_ : Rel A ℓ₂
   x ¬# y = ¬ (x # y)
+
+record IsTightApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isApartnessRelation : IsApartnessRelation _#_
+    tight               : Tight _≈_ _#_
+
+  open IsApartnessRelation isApartnessRelation public