diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4940047ba8..13f67bc3b7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,10 @@ Highlights
 Bug-fixes
 ---------
 
+* In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation`
+  to `#-sym` in order to avoid overloaded projection.
+  `irrefl` and `cotrans` are similarly renamed for the sake of consistency.
+
 Non-backwards compatible changes
 --------------------------------
 
diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
index d8b3ffcdfd..713edba00c 100644
--- a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
+++ b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
@@ -64,30 +64,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 x#z = helper (#⇒invertible x#z)
   where
diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda
index a8c5c88982..6ebee66787 100644
--- a/src/Algebra/Apartness/Structures.agda
+++ b/src/Algebra/Apartness/Structures.agda
@@ -34,6 +34,11 @@ record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
 
   open IsCommutativeRing isCommutativeRing public
   open IsApartnessRelation isApartnessRelation public
+    renaming
+      ( irrefl  to #-irrefl
+      ; sym     to #-sym
+      ; cotrans to #-cotrans
+      )
 
   field
     #⇒invertible : ∀ {x y} → x # y → Invertible 1# _*_ (x - y)