From ca13325653d85d0b6b23f9c0b742a9bee372f210 Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Fri, 7 Feb 2025 08:58:47 -0500 Subject: [PATCH 1/8] rename apartness sym to #-sym --- src/Algebra/Apartness/Structures.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda index a8c5c88982..c0cab7594a 100644 --- a/src/Algebra/Apartness/Structures.agda +++ b/src/Algebra/Apartness/Structures.agda @@ -33,7 +33,8 @@ record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where isApartnessRelation : IsApartnessRelation _≈_ _#_ open IsCommutativeRing isCommutativeRing public - open IsApartnessRelation isApartnessRelation public + open IsApartnessRelation isApartnessRelation public + renaming (sym to #-sym) field #⇒invertible : ∀ {x y} → x # y → Invertible 1# _*_ (x - y) From b7400ecef4fb4bfb11b3265da17f1758aba50032 Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Fri, 7 Feb 2025 08:58:56 -0500 Subject: [PATCH 2/8] update CHANGLOG --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4940047ba8..c83a718fb8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,10 @@ Non-backwards compatible changes Minor improvements ------------------ +* In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation` + to `#-sym` in order to avoid overloaded projection. + + Deprecated modules ------------------ From 8df40b5d8fb5433ea35517bb8f1cc0292f5d322e Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Fri, 7 Feb 2025 09:05:07 -0500 Subject: [PATCH 3/8] fix ws --- src/Algebra/Apartness/Structures.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda index c0cab7594a..2026e43692 100644 --- a/src/Algebra/Apartness/Structures.agda +++ b/src/Algebra/Apartness/Structures.agda @@ -33,7 +33,7 @@ record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where isApartnessRelation : IsApartnessRelation _≈_ _#_ open IsCommutativeRing isCommutativeRing public - open IsApartnessRelation isApartnessRelation public + open IsApartnessRelation isApartnessRelation public renaming (sym to #-sym) field From 3d0513599c1ac83b11df810330ede0dce37a8060 Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Fri, 7 Feb 2025 09:06:52 -0500 Subject: [PATCH 4/8] remove redundant #-sym --- .../Properties/HeytingCommutativeRing.agda | 24 ------------------- 1 file changed, 24 deletions(-) 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 From eec9196a9a6c72ad920b27272c1e36f6308ac08d Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Wed, 12 Feb 2025 11:17:55 -0500 Subject: [PATCH 5/8] rename other imports --- src/Algebra/Apartness/Structures.agda | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda index 2026e43692..f4979456ac 100644 --- a/src/Algebra/Apartness/Structures.agda +++ b/src/Algebra/Apartness/Structures.agda @@ -34,7 +34,11 @@ record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where open IsCommutativeRing isCommutativeRing public open IsApartnessRelation isApartnessRelation public - renaming (sym to #-sym) + renaming + ( irrefl to #-irrefl + ; sym to #-sym + ; cotrans to #-cotrans + ) field #⇒invertible : ∀ {x y} → x # y → Invertible 1# _*_ (x - y) From d5d902bbe3cd2d80f55b59f0f9ec9ea219c776c6 Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Wed, 12 Feb 2025 11:18:24 -0500 Subject: [PATCH 6/8] move to bug-fixes --- CHANGELOG.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c83a718fb8..fddda9cb09 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,16 +9,16 @@ 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. + Non-backwards compatible changes -------------------------------- Minor improvements ------------------ -* In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation` - to `#-sym` in order to avoid overloaded projection. - - Deprecated modules ------------------ From 935baac3aac3eab9f34ecfa564d6d98aba157091 Mon Sep 17 00:00:00 2001 From: Bradley Saul Date: Wed, 12 Feb 2025 11:20:46 -0500 Subject: [PATCH 7/8] fix ws --- src/Algebra/Apartness/Structures.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda index f4979456ac..6ebee66787 100644 --- a/src/Algebra/Apartness/Structures.agda +++ b/src/Algebra/Apartness/Structures.agda @@ -34,10 +34,10 @@ record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where open IsCommutativeRing isCommutativeRing public open IsApartnessRelation isApartnessRelation public - renaming + renaming ( irrefl to #-irrefl ; sym to #-sym - ; cotrans to #-cotrans + ; cotrans to #-cotrans ) field From e044e444e6fd9e8005779654937f564f7222bae0 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Thu, 13 Feb 2025 00:16:57 +0000 Subject: [PATCH 8/8] Update CHANGELOG.md --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fddda9cb09..13f67bc3b7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,7 +11,7 @@ Bug-fixes * In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation` to `#-sym` in order to avoid overloaded projection. - `irrefl` and `cotrans` are similarly renamed. + `irrefl` and `cotrans` are similarly renamed for the sake of consistency. Non-backwards compatible changes --------------------------------