From 592aeea63f43106f2e732f29b72d7209d69b9651 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 24 Oct 2022 13:21:36 +0100
Subject: [PATCH 01/14] added raw bundles

---
 src/Data/Nat/Base.agda | 28 +++++++++++++++++++++++++++-
 1 file changed, 27 insertions(+), 1 deletion(-)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 2f2a66edab..04246c3585 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -11,7 +11,7 @@
 
 module Data.Nat.Base where
 
-open import Algebra.Bundles.Raw using (RawMagma; RawMonoid)
+open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring)
 open import Data.Bool.Base using (Bool; true; false; T; not)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
@@ -323,3 +323,29 @@ compare (suc m) (suc n) with compare m n
   ; _∙_ = _+_
   ; ε   = 0
   }
+
+*-rawMagma : RawMagma 0ℓ 0ℓ
+*-rawMagma = record { _≈_ = _≡_ ; _∙_ = _*_ }
+
+*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
+*-1-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _*_ ; ε = 1 }
+
++-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ
++-*-rawNearSemiring = record
+  { Carrier = _
+  ; _≈_ = _≡_
+  ; _+_ = _+_
+  ; _*_ = _*_
+  ; 0# = 0
+  }
+
++-*-rawSemiring : RawSemiring 0ℓ 0ℓ
++-*-rawSemiring = record
+  { Carrier = _
+  ; _≈_ = _≡_
+  ; _+_ = _+_
+  ; _*_ = _*_
+  ; 0# = 0
+  ; 1# = 1
+  }
+

From 71efef8c8f13b70e2d28c8550b0db32560c28cd8 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 24 Oct 2022 13:30:26 +0100
Subject: [PATCH 02/14] [fix] added raw bundles (agda#1858)

---
 src/Data/Nat/Base.agda | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 04246c3585..abdd5bbe8a 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -325,10 +325,17 @@ compare (suc m) (suc n) with compare m n
   }
 
 *-rawMagma : RawMagma 0ℓ 0ℓ
-*-rawMagma = record { _≈_ = _≡_ ; _∙_ = _*_ }
+*-rawMagma = record
+  { _≈_ = _≡_
+  ; _∙_ = _*_
+  }
 
 *-1-rawMonoid : RawMonoid 0ℓ 0ℓ
-*-1-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _*_ ; ε = 1 }
+*-1-rawMonoid = record
+  { _≈_ = _≡_
+  ; _∙_ = _*_
+  ; ε = 1
+  }
 
 +-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ
 +-*-rawNearSemiring = record

From 4a0da553a44b05ca963e107ab194a32f98a33325 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 24 Oct 2022 14:05:20 +0100
Subject: [PATCH 03/14] removed duplicate bundle from

---
 src/Data/Nat/Properties.agda | 13 -------------
 1 file changed, 13 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 6839ee5579..ea83525e62 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -845,19 +845,6 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
 ------------------------------------------------------------------------
 -- Bundles
 
-*-rawMagma : RawMagma 0ℓ 0ℓ
-*-rawMagma = record
-  { _≈_ = _≡_
-  ; _∙_ = _*_
-  }
-
-*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
-*-1-rawMonoid = record
-  { _≈_ = _≡_
-  ; _∙_ = _*_
-  ; ε   = 1
-  }
-
 *-magma : Magma 0ℓ 0ℓ
 *-magma = record
   { isMagma = *-isMagma

From 42f5c0f7bfa8e3e2a55242016a217d12693ad98f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 24 Oct 2022 14:23:54 +0100
Subject: [PATCH 04/14] knock-on change to `Data.Nat.Binary.Properties`

---
 src/Data/Nat/Binary/Properties.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index 2f79568895..67718af6b9 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -983,19 +983,19 @@ toℕ-homo-* x y =  aux x y (size x ℕ.+ size y) ℕₚ.≤-refl
     |y|+1+|x|≤cnt = subst (ℕ._≤ cnt) eq |x|+1+|y|≤cnt
 
 
-toℕ-isMagmaHomomorphism-* : IsMagmaHomomorphism *-rawMagma ℕₚ.*-rawMagma toℕ
+toℕ-isMagmaHomomorphism-* : IsMagmaHomomorphism *-rawMagma ℕᵇ.*-rawMagma toℕ
 toℕ-isMagmaHomomorphism-* = record
   { isRelHomomorphism = toℕ-isRelHomomorphism
   ; homo              = toℕ-homo-*
   }
 
-toℕ-isMonoidHomomorphism-* : IsMonoidHomomorphism *-1-rawMonoid ℕₚ.*-1-rawMonoid toℕ
+toℕ-isMonoidHomomorphism-* : IsMonoidHomomorphism *-1-rawMonoid ℕᵇ.*-1-rawMonoid toℕ
 toℕ-isMonoidHomomorphism-* = record
   { isMagmaHomomorphism = toℕ-isMagmaHomomorphism-*
   ; ε-homo              = refl
   }
 
-toℕ-isMonoidMonomorphism-* : IsMonoidMonomorphism *-1-rawMonoid ℕₚ.*-1-rawMonoid toℕ
+toℕ-isMonoidMonomorphism-* : IsMonoidMonomorphism *-1-rawMonoid ℕᵇ.*-1-rawMonoid toℕ
 toℕ-isMonoidMonomorphism-* = record
   { isMonoidHomomorphism = toℕ-isMonoidHomomorphism-*
   ; injective            = toℕ-injective

From aebe3e7d3bf1c1fe3933fd4b5603f2ced1302fcd Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 24 Oct 2022 16:03:56 +0100
Subject: [PATCH 05/14] updated CHANGELOG

---
 CHANGELOG.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 02014e8d9f..58ca827765 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1739,6 +1739,13 @@ Other minor changes
   _⊓′_ : ℕ → ℕ → ℕ
   ∣_-_∣′ : ℕ → ℕ → ℕ
   _! : ℕ → ℕ
+
+  +-rawMagma          : RawMagma 0ℓ 0ℓ
+  +-0-rawMonoid       : RawMonoid 0ℓ 0ℓ
+  *-rawMagma          : RawMagma 0ℓ 0ℓ
+  *-1-rawMonoid       : RawMonoid 0ℓ 0ℓ
+  +-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ
+  +-*-rawSemiring     : RawSemiring 0ℓ 0ℓ
   ```
 
 

From 8f5de045538e913e7ac900c7e68eaba8275ac890 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 25 Oct 2022 10:43:54 +0100
Subject: [PATCH 06/14] [fix] issue #1865 for `Data.Nat`

---
 src/Data/Nat/Properties.agda | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index ea83525e62..6a5c88a192 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -2289,3 +2289,7 @@ suc[pred[n]]≡n {suc n} _   = refl
 {-# WARNING_ON_USAGE <-step
 "Warning: <-step was deprecated in v2.0. Please use m<n⇒m<1+n instead. "
 #-}
+
+{- issue1844/issue1755: raw bundles have moved to `Data.X.Base` -}
+open Data.Nat.Base public
+  using (*-rawMagma; *-1-rawMonoid)

From 31079672868aa7247b28f5b01cba9ef8e25b8db6 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Wed, 26 Oct 2022 04:22:52 +0100
Subject: [PATCH 07/14] Fix #1844 by renaming abelian group proof for integers
 and moving raw bundles (#1862)

---
 CHANGELOG.md                     |  2 ++
 src/Data/Integer/Base.agda       | 48 ++++++++++++++++++++++++++++++++
 src/Data/Integer/Properties.agda | 22 ++++++++-------
 3 files changed, 62 insertions(+), 10 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 58ca827765..e4ca38e3a5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -946,6 +946,8 @@ Deprecated names
   pos-distrib-* ↦ pos-*
   pos-+-commute ↦ pos-+
   abs-*-commute ↦ abs-*
+  
+  +-isAbelianGroup ↦ +-0-isAbelianGroup
   ```
   
 * In `Data.List.Properties`:
diff --git a/src/Data/Integer/Base.agda b/src/Data/Integer/Base.agda
index 8b81cddd29..4432615c77 100644
--- a/src/Data/Integer/Base.agda
+++ b/src/Data/Integer/Base.agda
@@ -11,6 +11,8 @@
 
 module Data.Integer.Base where
 
+open import Algebra.Bundles.Raw
+  using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing)
 open import Data.Bool.Base using (Bool; T; true; false)
 open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s)
 open import Data.Sign.Base as Sign using (Sign)
@@ -293,3 +295,49 @@ _%ℕ_ : (dividend : ℤ) (divisor : ℕ) .{{_ : ℕ.NonZero divisor}} → ℕ
 
 _%_ : (dividend divisor : ℤ) .{{_ : NonZero divisor}} → ℕ
 i % j = i %ℕ ∣ j ∣
+
+------------------------------------------------------------------------
+-- Bundles
+
++-rawMagma : RawMagma 0ℓ 0ℓ
++-rawMagma = record { _≈_ = _≡_ ; _∙_ = _+_ }
+
++-0-rawMonoid : RawMonoid 0ℓ 0ℓ
++-0-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _+_ ; ε = 0ℤ }
+
+*-rawMagma : RawMagma 0ℓ 0ℓ
+*-rawMagma = record { _≈_ = _≡_ ; _∙_ = _*_ }
+
+*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
+*-1-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _*_ ; ε = 1ℤ }
+
++-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ
++-*-rawNearSemiring = record
+  { Carrier = _
+  ; _≈_ = _≡_
+  ; _+_ = _+_
+  ; _*_ = _*_
+  ; 0# = 0ℤ
+  }
+
++-*-rawSemiring : RawSemiring 0ℓ 0ℓ
++-*-rawSemiring = record
+  { Carrier = _
+  ; _≈_ = _≡_
+  ; _+_ = _+_
+  ; _*_ = _*_
+  ; 0# = 0ℤ
+  ; 1# = 1ℤ
+  }
+
++-*-rawRing : RawRing 0ℓ 0ℓ
++-*-rawRing = record
+  { Carrier = _
+  ; _≈_ = _≡_
+  ; _+_ = _+_
+  ; _*_ = _*_
+  ; -_ = -_
+  ; 0# = 0ℤ
+  ; 1# = 1ℤ
+  }
+
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index fa313d91f0..812347aea4 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -944,8 +944,8 @@ distribʳ-⊖-+-neg m n o = begin
   ; ⁻¹-cong  = cong (-_)
   }
 
-+-isAbelianGroup : IsAbelianGroup _+_ +0 (-_)
-+-isAbelianGroup = record
++-0-isAbelianGroup : IsAbelianGroup _+_ +0 (-_)
++-0-isAbelianGroup = record
   { isGroup = +-0-isGroup
   ; comm    = +-comm
   }
@@ -980,7 +980,7 @@ distribʳ-⊖-+-neg m n o = begin
 
 +-0-abelianGroup : AbelianGroup 0ℓ 0ℓ
 +-0-abelianGroup = record
-  { isAbelianGroup = +-isAbelianGroup
+  { isAbelianGroup = +-0-isAbelianGroup
   }
 
 ------------------------------------------------------------------------
@@ -1522,7 +1522,7 @@ private
 
 +-*-isRing : IsRing _+_ _*_ -_ 0ℤ 1ℤ
 +-*-isRing = record
-  { +-isAbelianGroup = +-isAbelianGroup
+  { +-isAbelianGroup = +-0-isAbelianGroup
   ; *-cong           = cong₂ _*_
   ; *-assoc          = *-assoc
   ; *-identity       = *-identity
@@ -1539,12 +1539,6 @@ private
 ------------------------------------------------------------------------
 -- Bundles
 
-*-rawMagma : RawMagma 0ℓ 0ℓ
-*-rawMagma = record { _≈_ = _≡_ ; _∙_ = _*_ }
-
-*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
-*-1-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _*_ ; ε = 1ℤ }
-
 *-magma : Magma 0ℓ 0ℓ
 *-magma = record
   { isMagma = *-isMagma
@@ -2387,3 +2381,11 @@ pos-distrib-* m n = sym (pos-* m n)
 "Warning: pos-distrib-* was deprecated in v2.0
 Please use pos-* instead."
 #-}
++-isAbelianGroup = +-0-isAbelianGroup
+{-# WARNING_ON_USAGE +-isAbelianGroup
+"Warning: +-isAbelianGroup was deprecated in v2.0
+Please use +-0-isAbelianGroup instead."
+#-}
+{- issue1844/issue1755: raw bundles have moved to `Data.X.Base` -}
+open Data.Integer.Base public
+  using (*-rawMagma; *-1-rawMonoid)

From e4f4e158f871750f1709f6f7c708c3f8632737af Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 26 Oct 2022 19:05:15 +0100
Subject: [PATCH 08/14] [fix] issue #1865 for remaining bundles of #1755

---
 src/Data/Nat/Binary/Properties.agda            | 6 ++++++
 src/Data/Rational/Properties.agda              | 5 +++++
 src/Data/Rational/Unnormalised/Properties.agda | 5 +++++
 3 files changed, 16 insertions(+)

diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index 67718af6b9..8816eeb735 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -1499,3 +1499,9 @@ Please use +-*-semiring instead."
 "Warning: *-+-commutativeSemiring was deprecated in v1.4.
 Please use +-*-commutativeSemiring instead."
 #-}
+
+-- Version 2.0
+
+{- issue1858/issue1755: raw bundles have moved to `Data.X.Base` -}
+open Data.Nat.Binary.Base public
+  using (+-rawMagma; +-0-rawMonoid; *-rawMagma; *-1-rawMonoid)
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 6826094088..d922409552 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -1687,3 +1687,8 @@ negative<positive {p} {q} p<0 q>0 = neg<pos p q {{p<0}} {{q>0}}
 "Warning: negative<positive was deprecated in v2.0.
 Please use neg<pos instead."
 #-}
+
+{- issue1865/issue1755: raw bundles have moved to `Data.X.Base` -}
+open Data.Rational.Base public
+  using (+-rawMagma; +-rawMonoid; +-0-rawGroup; *-rawMagma; *-rawMonoid;
+  +-*-rawNearSemiring; +-*-rawSemiring; +-*-rawRing)
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 5dc3d4d2bc..f040651e82 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -1843,3 +1843,8 @@ negative<positive {p} {q} p<0 q>0 = neg<pos p q {{p<0}} {{q>0}}
 "Warning: negative<positive was deprecated in v2.0.
 Please use neg<pos instead."
 #-}
+
+{- issue1865/issue1755: raw bundles have moved to `Data.X.Base` -}
+open Data.Rational.Unnormalised.Base public
+  using (+-rawMagma; +-rawMonoid; +-0-rawGroup; *-rawMagma; *-rawMonoid;
+  +-*-rawNearSemiring; +-*-rawSemiring; +-*-rawRing)

From 92e3548fda607729040c24dc85df03834946128a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 26 Oct 2022 19:18:07 +0100
Subject: [PATCH 09/14] added `+-0-rawGroup`

---
 src/Data/Integer/Base.agda | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Data/Integer/Base.agda b/src/Data/Integer/Base.agda
index 4432615c77..ade66aa73a 100644
--- a/src/Data/Integer/Base.agda
+++ b/src/Data/Integer/Base.agda
@@ -12,7 +12,7 @@
 module Data.Integer.Base where
 
 open import Algebra.Bundles.Raw
-  using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing)
+  using (RawMagma; RawMonoid; RawGroup; RawNearSemiring; RawSemiring; RawRing)
 open import Data.Bool.Base using (Bool; T; true; false)
 open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s)
 open import Data.Sign.Base as Sign using (Sign)
@@ -305,6 +305,9 @@ i % j = i %ℕ ∣ j ∣
 +-0-rawMonoid : RawMonoid 0ℓ 0ℓ
 +-0-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _+_ ; ε = 0ℤ }
 
++-0-rawGroup : RawGroup 0ℓ 0ℓ
++-0-rawGroup = record { _≈_ = _≡_ ; _∙_ = _+_ ; _⁻¹ = -_; ε = 0ℤ }
+
 *-rawMagma : RawMagma 0ℓ 0ℓ
 *-rawMagma = record { _≈_ = _≡_ ; _∙_ = _*_ }
 

From 5e60315b3bd017f1c0fc196edb458cfd914229dc Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 26 Oct 2022 19:39:26 +0100
Subject: [PATCH 10/14] deprecated `+-rawMonoid` and `*-raw-Monoid`

---
 src/Data/Rational/Base.agda       | 28 ++++++++++++++++++++++++----
 src/Data/Rational/Properties.agda |  6 +++---
 2 files changed, 27 insertions(+), 7 deletions(-)

diff --git a/src/Data/Rational/Base.agda b/src/Data/Rational/Base.agda
index d973ec231a..1dd7c646bc 100644
--- a/src/Data/Rational/Base.agda
+++ b/src/Data/Rational/Base.agda
@@ -286,8 +286,8 @@ syntax truncate p = [ p ]
   ; _∙_ = _+_
   }
 
-+-rawMonoid : RawMonoid 0ℓ 0ℓ
-+-rawMonoid = record
++-0-rawMonoid : RawMonoid 0ℓ 0ℓ
++-0-rawMonoid = record
   { _≈_ = _≡_
   ; _∙_ = _+_
   ; ε   = 0ℚ
@@ -334,9 +334,29 @@ syntax truncate p = [ p ]
   ; _∙_ = _*_
   }
 
-*-rawMonoid : RawMonoid 0ℓ 0ℓ
-*-rawMonoid = record
+*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
+*-1-rawMonoid = record
   { _≈_ = _≡_
   ; _∙_ = _*_
   ; ε   = 1ℚ
   }
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
++-rawMonoid = +-0-rawMonoid
+{-# WARNING_ON_USAGE +-rawMonoid
+"Warning: +-rawMonoid was deprecated in v2.0
+Please use +-0-rawMonoid instead."
+#-}
+*-rawMonoid = *-1-rawMonoid
+{-# WARNING_ON_USAGE *-rawMonoid
+"Warning: *-rawMonoid was deprecated in v2.0
+Please use *-1-rawMonoid instead."
+#-}
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index d922409552..45e98ded0f 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -5,6 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for +-rawMonoid, *-rawMonoid (issue #1865, #1844, #1755)
 
 module Data.Rational.Properties where
 
@@ -1687,8 +1688,7 @@ negative<positive {p} {q} p<0 q>0 = neg<pos p q {{p<0}} {{q>0}}
 "Warning: negative<positive was deprecated in v2.0.
 Please use neg<pos instead."
 #-}
-
 {- issue1865/issue1755: raw bundles have moved to `Data.X.Base` -}
 open Data.Rational.Base public
-  using (+-rawMagma; +-rawMonoid; +-0-rawGroup; *-rawMagma; *-rawMonoid;
-  +-*-rawNearSemiring; +-*-rawSemiring; +-*-rawRing)
+  using (+-rawMagma; +-0-rawGroup; *-rawMagma; +-*-rawNearSemiring; +-*-rawSemiring; +-*-rawRing)
+  renaming (+-0-rawMonoid to +-rawMonoid; *-1-rawMonoid to *-rawMonoid)

From b5e0ecd839fbde7c2237a95d35c40db1d89724d7 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 26 Oct 2022 19:42:11 +0100
Subject: [PATCH 11/14] deprecated `+-rawMonoid` and `*-raw-Monoid`

---
 src/Data/Rational/Unnormalised/Base.agda      | 27 ++++++++++++++++---
 .../Rational/Unnormalised/Properties.agda     |  6 +++--
 2 files changed, 27 insertions(+), 6 deletions(-)

diff --git a/src/Data/Rational/Unnormalised/Base.agda b/src/Data/Rational/Unnormalised/Base.agda
index e146b809af..03a2eff34a 100644
--- a/src/Data/Rational/Unnormalised/Base.agda
+++ b/src/Data/Rational/Unnormalised/Base.agda
@@ -297,8 +297,8 @@ syntax truncate p = [ p ]
   ; _∙_ = _+_
   }
 
-+-rawMonoid : RawMonoid 0ℓ 0ℓ
-+-rawMonoid = record
++-0-rawMonoid : RawMonoid 0ℓ 0ℓ
++-0-rawMonoid = record
   { _≈_ = _≃_
   ; _∙_ = _+_
   ; ε   = 0ℚᵘ
@@ -352,9 +352,28 @@ syntax truncate p = [ p ]
   ; _∙_ = _*_
   }
 
-*-rawMonoid : RawMonoid 0ℓ 0ℓ
-*-rawMonoid = record
+*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
+*-1-rawMonoid = record
   { _≈_ = _≃_
   ; _∙_ = _*_
   ; ε   = 1ℚᵘ
   }
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
++-rawMonoid = +-0-rawMonoid
+{-# WARNING_ON_USAGE +-rawMonoid
+"Warning: +-rawMonoid was deprecated in v2.0
+Please use +-0-rawMonoid instead."
+#-}
+*-rawMonoid = *-1-rawMonoid
+{-# WARNING_ON_USAGE *-rawMonoid
+"Warning: *-rawMonoid was deprecated in v2.0
+Please use *-1-rawMonoid instead."
+#-}
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index f040651e82..356ee69806 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -5,6 +5,8 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for +-rawMonoid, *-rawMonoid (issue #1865, #1844, #1755)
+
 
 module Data.Rational.Unnormalised.Properties where
 
@@ -1846,5 +1848,5 @@ Please use neg<pos instead."
 
 {- issue1865/issue1755: raw bundles have moved to `Data.X.Base` -}
 open Data.Rational.Unnormalised.Base public
-  using (+-rawMagma; +-rawMonoid; +-0-rawGroup; *-rawMagma; *-rawMonoid;
-  +-*-rawNearSemiring; +-*-rawSemiring; +-*-rawRing)
+  using (+-rawMagma; +-0-rawGroup; *-rawMagma; +-*-rawNearSemiring; +-*-rawSemiring; +-*-rawRing)
+  renaming (+-0-rawMonoid to +-rawMonoid; *-1-rawMonoid to *-rawMonoid)

From 3617f7dcb5454e57612081b3512a1cc1d7bf3948 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 26 Oct 2022 19:52:45 +0100
Subject: [PATCH 12/14] updated `CHANGELOG`

---
 CHANGELOG.md                      | 22 ++++++++++++++++++----
 src/Data/Rational/Properties.agda |  8 ++++----
 2 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e4ca38e3a5..fe6f3b5922 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1036,6 +1036,12 @@ Deprecated names
   negative<positive     ↦ neg<pos
   ```
 
+* In `Data.Rational.Base`:
+  ```
+  +-rawMonoid ↦ +-0-rawMonoid
+  *-rawMonoid ↦ *-1-rawMonoid
+  ```
+
 * In `Data.Rational.Properties`:
   ```
   *-monoʳ-≤-neg    ↦  *-monoʳ-≤-nonPos
@@ -1050,6 +1056,12 @@ Deprecated names
   negative<positive     ↦ neg<pos
   ```
 
+* In `Data.Rational.Unnormalised.Base`:
+  ```
+  +-rawMonoid ↦ +-0-rawMonoid
+  *-rawMonoid ↦ *-1-rawMonoid
+  ```
+
 * In `Data.Sum.Properties`:
   ```agda
   [,]-∘-distr      ↦  [,]-∘
@@ -1655,7 +1667,12 @@ Other minor changes
 * Added new functions in `Data.Integer.Base`:
   ```
   _^_ : ℤ → ℕ → ℤ
-  ```
+ 
+  +-0-rawGroup  : Rawgroup 0ℓ 0ℓ
+
+  *-rawMagma    : RawMagma 0ℓ 0ℓ
+  *-1-rawMonoid : RawMonoid 0ℓ 0ℓ
+ ```
 
 * Added new proofs in `Data.Integer.Properties`:
   ```agda
@@ -1670,9 +1687,6 @@ Other minor changes
   ^-*-assoc      : (i ^ m) ^ n ≡ i ^ (m ℕ.* n)
   ^-distribˡ-+-* : i ^ (m ℕ.+ n) ≡ i ^ m * i ^ n
 
-  *-rawMagma    : RawMagma 0ℓ 0ℓ
-  *-1-rawMonoid : RawMonoid 0ℓ 0ℓ
-
   ^-isMagmaHomomorphism  : IsMagmaHomomorphism  ℕ.+-rawMagma    *-rawMagma    (i ^_)
   ^-isMonoidHomomorphism : IsMonoidHomomorphism ℕ.+-0-rawMonoid *-1-rawMonoid (i ^_)
   ```
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 45e98ded0f..aa8108d58e 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -826,13 +826,13 @@ toℚᵘ-isMagmaHomomorphism-+ = record
   ; homo              = toℚᵘ-homo-+
   }
 
-toℚᵘ-isMonoidHomomorphism-+ : IsMonoidHomomorphism +-rawMonoid ℚᵘ.+-rawMonoid toℚᵘ
+toℚᵘ-isMonoidHomomorphism-+ : IsMonoidHomomorphism +-0-rawMonoid ℚᵘ.+-0-rawMonoid toℚᵘ
 toℚᵘ-isMonoidHomomorphism-+ = record
   { isMagmaHomomorphism = toℚᵘ-isMagmaHomomorphism-+
   ; ε-homo              = ℚᵘ.≃-refl
   }
 
-toℚᵘ-isMonoidMonomorphism-+ : IsMonoidMonomorphism +-rawMonoid ℚᵘ.+-rawMonoid toℚᵘ
+toℚᵘ-isMonoidMonomorphism-+ : IsMonoidMonomorphism +-0-rawMonoid ℚᵘ.+-0-rawMonoid toℚᵘ
 toℚᵘ-isMonoidMonomorphism-+ = record
   { isMonoidHomomorphism = toℚᵘ-isMonoidHomomorphism-+
   ; injective            = toℚᵘ-injective
@@ -1041,13 +1041,13 @@ toℚᵘ-isMagmaHomomorphism-* = record
   ; homo              = toℚᵘ-homo-*
   }
 
-toℚᵘ-isMonoidHomomorphism-* : IsMonoidHomomorphism *-rawMonoid ℚᵘ.*-rawMonoid toℚᵘ
+toℚᵘ-isMonoidHomomorphism-* : IsMonoidHomomorphism *-1-rawMonoid ℚᵘ.*-1-rawMonoid toℚᵘ
 toℚᵘ-isMonoidHomomorphism-* = record
   { isMagmaHomomorphism = toℚᵘ-isMagmaHomomorphism-*
   ; ε-homo              = ℚᵘ.≃-refl
   }
 
-toℚᵘ-isMonoidMonomorphism-* : IsMonoidMonomorphism *-rawMonoid ℚᵘ.*-rawMonoid toℚᵘ
+toℚᵘ-isMonoidMonomorphism-* : IsMonoidMonomorphism *-1-rawMonoid ℚᵘ.*-1-rawMonoid toℚᵘ
 toℚᵘ-isMonoidMonomorphism-* = record
   { isMonoidHomomorphism = toℚᵘ-isMonoidHomomorphism-*
   ; injective            = toℚᵘ-injective

From 22b1c3d6e4a41d490adc8ec0680ff55b821543b4 Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Sun, 30 Oct 2022 13:13:56 +0000
Subject: [PATCH 13/14] Update Base.agda

Used the web-interface and screwed it up, first time around. Yuk. :facepalm:
---
 src/Data/Integer/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Integer/Base.agda b/src/Data/Integer/Base.agda
index cb67673985..ade66aa73a 100644
--- a/src/Data/Integer/Base.agda
+++ b/src/Data/Integer/Base.agda
@@ -305,7 +305,7 @@ i % j = i %ℕ ∣ j ∣
 +-0-rawMonoid : RawMonoid 0ℓ 0ℓ
 +-0-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _+_ ; ε = 0ℤ }
 
--0-rawGroup : RawGroup 0ℓ 0ℓ
++-0-rawGroup : RawGroup 0ℓ 0ℓ
 +-0-rawGroup = record { _≈_ = _≡_ ; _∙_ = _+_ ; _⁻¹ = -_; ε = 0ℤ }
 
 *-rawMagma : RawMagma 0ℓ 0ℓ

From 9a083ab7143274259a293dc41c05361671bb9d6f Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Mon, 7 Nov 2022 11:49:20 +0000
Subject: [PATCH 14/14] Update CHANGELOG.md

Reinstated lost addition of `parity`. Hope this fixes :facepalm:
---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e551d44643..89aaa9f0f3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1829,6 +1829,8 @@ Other minor changes
   ∣_-_∣′ : ℕ → ℕ → ℕ
   _! : ℕ → ℕ
 
+  parity : ℕ → Parity
+  
   +-rawMagma          : RawMagma 0ℓ 0ℓ
   +-0-rawMonoid       : RawMonoid 0ℓ 0ℓ
   *-rawMagma          : RawMagma 0ℓ 0ℓ