The free Magma on a Set, resp. Setoid [bis]

CHANGELOG.md

@@ -78,6 +78,12 @@ Deprecated names
 New modules
 -----------
 
+* Algebraic structures obtained as the free thing (for their signature):
+  ```
+  Algebra.Free
+  Algebra.Free.Magma
+  ```
+
 * Raw bundles for module-like algebraic structures:
   ```
   Algebra.Module.Bundles.Raw
@@ -93,6 +99,11 @@ New modules
   Induction.InfiniteDescent
   ```
 
+* Bundled morphisms between algebraic structures:
+  ```
+  Algebra.Morphism.Bundles
+ ```
+
 * The unique morphism from the initial, resp. terminal, algebra:
   ```agda
   Algebra.Morphism.Construct.Initial
@@ -229,6 +240,17 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
+* In `Algebra.Morphism.Construct.Composition`:
+  ```
+  magmaHomomorphism : MagmaHomomorphism M₁ M₂ → MagmaHomomorphism M₂ M₃ →
+                      MagmaHomomorphism M₁ M₃
+  ```
+
+* In `Algebra.Morphism.Construct.Identity`:
+  ```
+  magmaHomomorphism : MagmaHomomorphism M M
+  ```
+
 * In `Algebra.Morphism.Structures`
   ```agda
   module SuccessorSetMorphisms (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂) where

src/Algebra/Free.agda

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