The free Magma on a Set, resp. Setoid

CHANGELOG.md

@@ -427,6 +427,32 @@ Non-backwards compatible changes
   Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n
   ```
 
+### Change in the definition of `_≤″_` (issue #1919)
+
+* The definition of `_≤″_` in `Data.Nat.Base` was previously:
+  ```agda
+  record _≤″_ (m n : ℕ) : Set where
+    constructor less-than-or-equal
+    field
+      {k}   : ℕ
+      proof : m + k ≡ n
+  ```
+  which introduced a spurious additional definition, when this is in fact, modulo
+  field names and implicit/explicit qualifiers, equivalent to the definition of left-
+  divisibility, `_∣ˡ_` for the `RawMagma` structure of `_+_`. Since the addition of
+  raw bundles to `Data.X.Base`, this definition can now be made directly. Knock-on
+  consequences include the need to retain the old constructor name, now introduced
+  as a pattern synonym, and deprecation of (a function equiavlent to) the former
+  field name/projection function `proof`. 
+
+* Accordingly, the definition has been changed to:
+  ```agda
+  _≤″_ : (m n : ℕ)  → Set
+  _≤″_ = _∣ˡ_ +-rawMagma
+
+  pattern less-than-or-equal {k} proof = k , proof
+  ```
+
 ### Renaming of `Reflection` modules
 
 * Under the `Reflection` module, there were various impending name clashes
@@ -1109,6 +1135,11 @@ Deprecated names
   map-with-∈↔  ↦  mapWith∈↔
   ```
 
+* In `Data.Nat.Base`:
+  ```
+  _≤″_.proof ↦  proj₂
+  ```
+
 * In `Data.Nat.Properties`:
   ```
   suc[pred[n]]≡n  ↦  suc-pred
@@ -1325,6 +1356,12 @@ New modules
   Algebra.Construct.Flip.Op
   ```
 
+* Algebraic structures obtained as the free thing (for their signature):
+  ```
+  Algebra.Bundles.Free
+  Algebra.Bundles.Free.Magma
+  ```
+
 * Morphisms between module-like algebraic structures:
   ```
   Algebra.Module.Morphism.Construct.Composition

README/Design/Decidability.agda

@@ -11,7 +11,7 @@ module README.Design.Decidability where
 open import Data.Bool
 open import Data.List
 open import Data.List.Properties using (∷-injective)
-open import Data.Nat
+open import Data.Nat hiding (proof)
 open import Data.Nat.Properties using (suc-injective)
 open import Data.Product
 open import Data.Unit

src/Algebra/Bundles/Free.agda

@@ -0,0 +1,11 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions of 'pre-free' and 'free' bundles
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Algebra.Bundles.Free where
+
+open import Algebra.Bundles.Free.Magma public