fix: CHANGELOG plus tidying up

Author: jamesmckinna

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`.

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
 ------------------------------------------------------------------------

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#                    ∎
 

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