diff --git a/CHANGELOG.md b/CHANGELOG.md
index fcb907c03b..dda9229674 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -43,6 +43,12 @@ Splitting up `Data.Maybe` into the standard hierarchy.
   Eq-isDecEquivalence ↦ isDecEquivalence
   ```
 
+#### Changes to the algebra hierarchy
+
+* Added `Magma` and `IsMagma` to the algebra hierarchy.
+
+* The name `RawSemigroup` in `Algebra` has been deprecated in favour of `RawMagma`.
+
 #### Relaxation of ring solvers requirements
 
 * In the ring solvers below, the assumption that equality is `Decidable`
@@ -79,11 +85,27 @@ Deprecated features
 Other minor additions
 ---------------------
 
+* Added new records to `Algebra`:
+  ```agda
+  record RawMagma c ℓ : Set (suc (c ⊔ ℓ))
+  record Magma    c ℓ : Set (suc (c ⊔ ℓ))
+  ```
+
+* Added new proof to `Algebra.FunctionProperties.Consequences`:
+  ```agda
+  wlog : Commutative f → Total _R_ → (∀ a b → a R b → P (f a b)) → ∀ a b → P (f a b)
+  ```
+
 * Added new operator to `Algebra.Solver.Ring`.
   ```agda
   _:×_
   ```
 
+* Added new records to `Algebra.Structures`:
+  ```agda
+  record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ)
+  ```
+
 * Added new functions to `Codata.Stream`:
   ```agda
   splitAt    : (n : ℕ) → Stream A ∞ → Vec A n × Stream A ∞
@@ -96,11 +118,6 @@ Other minor additions
   splitAt-map : splitAt n (map f xs) ≡ map (map f) (map f) (splitAt n xs)
   ```
 
-* Added new proof to `Algebra.FunctionProperties.Consequences`:
-  ```agda
-  wlog : Commutative f → Total _R_ → (∀ a b → a R b → P (f a b)) → ∀ a b → P (f a b)
-  ```
-
 * Added new function to `Data.Fin.Base`:
   ```agda
   cast : m ≡ n → Fin m → Fin n
diff --git a/src/Algebra.agda b/src/Algebra.agda
index f3868d731f..59e18effdb 100644
--- a/src/Algebra.agda
+++ b/src/Algebra.agda
@@ -14,15 +14,32 @@ open import Function
 open import Level
 
 ------------------------------------------------------------------------
--- Semigroups
+-- Magmas
+
+record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∙_     : Op₂ Carrier
 
-record RawSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
+record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
   infix  4 _≈_
   field
     Carrier : Set c
     _≈_     : Rel Carrier ℓ
     _∙_     : Op₂ Carrier
+    isMagma : IsMagma _≈_ _∙_
+
+  open IsMagma isMagma public
+
+  rawMagma : RawMagma _ _
+  rawMagma = record { _≈_ = _≈_; _∙_ = _∙_ }
+
+------------------------------------------------------------------------
+-- Semigroups
 
 record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -35,11 +52,10 @@ record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open IsSemigroup isSemigroup public
 
-  rawSemigroup : RawSemigroup _ _
-  rawSemigroup = record
-    { _≈_ = _≈_
-    ; _∙_ = _∙_
-    }
+  magma : Magma c ℓ
+  magma = record { isMagma = isMagma }
+
+  open Magma magma public using (rawMagma)
 
 record Band c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -55,7 +71,7 @@ record Band c ℓ : Set (suc (c ⊔ ℓ)) where
   semigroup : Semigroup c ℓ
   semigroup = record { isSemigroup = isSemigroup }
 
-  open Semigroup semigroup public using (rawSemigroup)
+  open Semigroup semigroup public using (magma; rawMagma)
 
 ------------------------------------------------------------------------
 -- Monoids
@@ -87,11 +103,9 @@ record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
   semigroup = record { isSemigroup = isSemigroup }
 
   rawMonoid : RawMonoid _ _
-  rawMonoid = record
-    { _≈_ = _≈_
-    ; _∙_ = _∙_
-    ; ε   = ε
-    }
+  rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε}
+
+  open Semigroup semigroup public using (rawMagma; magma)
 
 record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -108,7 +122,7 @@ record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   monoid : Monoid _ _
   monoid = record { isMonoid = isMonoid }
 
-  open Monoid monoid public using (semigroup; rawMonoid)
+  open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)
 
 record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -126,7 +140,7 @@ record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
   commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
 
   open CommutativeMonoid commutativeMonoid public
-    using (semigroup; rawMonoid; monoid)
+    using (rawMagma; magma; semigroup; rawMonoid; monoid)
 
 ------------------------------------------------------------------------
 -- Groups
@@ -157,17 +171,12 @@ record Group c ℓ : Set (suc (c ⊔ ℓ)) where
   open IsGroup isGroup public
 
   rawGroup : RawGroup _ _
-  rawGroup = record
-    { _≈_ = _≈_
-    ; _∙_ = _∙_
-    ; ε   = ε
-    ; _⁻¹ = _⁻¹
-    }
+  rawGroup = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹}
 
   monoid : Monoid _ _
   monoid = record { isMonoid = isMonoid }
 
-  open Monoid monoid public using (semigroup; rawMonoid)
+  open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)
 
 record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 _⁻¹
@@ -187,7 +196,7 @@ record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
   group = record { isGroup = isGroup }
 
   open Group group public
-    using (semigroup; monoid; rawMonoid; rawGroup)
+    using (rawMagma; magma; semigroup; monoid; rawMonoid; rawGroup)
 
   commutativeMonoid : CommutativeMonoid _ _
   commutativeMonoid =
@@ -226,13 +235,24 @@ record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
   +-monoid = record { isMonoid = +-isMonoid }
 
   open Monoid +-monoid public
-         using ()
-         renaming ( semigroup to +-semigroup
-                  ; rawMonoid to +-rawMonoid)
+    using ()
+    renaming
+    ( rawMagma  to +-rawMagma
+    ; magma     to +-magma
+    ; semigroup to +-semigroup
+    ; rawMonoid to +-rawMonoid
+    )
 
   *-semigroup : Semigroup _ _
   *-semigroup = record { isSemigroup = *-isSemigroup }
 
+  open Semigroup *-semigroup public
+    using ()
+    renaming
+    ( rawMagma to *-rawMagma
+    ; magma    to *-magma
+    )
+
 record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _*_
   infixl 6 _+_
@@ -251,9 +271,10 @@ record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
   nearSemiring = record { isNearSemiring = isNearSemiring }
 
   open NearSemiring nearSemiring public
-         using ( +-semigroup; +-rawMonoid; +-monoid
-               ; *-semigroup
-               )
+    using
+    ( +-rawMagma; +-magma; +-semigroup; +-rawMonoid; +-monoid
+    ; *-rawMagma; *-magma; *-semigroup
+    )
 
   +-commutativeMonoid : CommutativeMonoid _ _
   +-commutativeMonoid =
@@ -281,20 +302,26 @@ record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
     record { isCommutativeMonoid = +-isCommutativeMonoid }
 
   open CommutativeMonoid +-commutativeMonoid public
-         using ()
-         renaming ( semigroup to +-semigroup
-                  ; rawMonoid to +-rawMonoid
-                  ; monoid    to +-monoid
-                  )
+    using ()
+    renaming
+    ( rawMagma  to +-rawMagma
+    ; magma     to +-magma
+    ; semigroup to +-semigroup
+    ; rawMonoid to +-rawMonoid
+    ; monoid    to +-monoid
+    )
 
   *-monoid : Monoid _ _
   *-monoid = record { isMonoid = *-isMonoid }
 
   open Monoid *-monoid public
-         using ()
-         renaming ( semigroup to *-semigroup
-                  ; rawMonoid to *-rawMonoid
-                  )
+    using ()
+    renaming
+    ( rawMagma  to *-rawMagma
+    ; magma     to *-magma
+    ; semigroup to *-semigroup
+    ; rawMonoid to *-rawMonoid
+    )
 
 record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _*_
@@ -328,17 +355,19 @@ record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open SemiringWithoutAnnihilatingZero
          semiringWithoutAnnihilatingZero public
-         using ( +-semigroup; +-rawMonoid; +-monoid
-               ; +-commutativeMonoid
-               ; *-semigroup; *-rawMonoid; *-monoid
-               )
+    using
+    ( +-rawMagma;  +-magma;  +-semigroup
+    ; *-rawMagma;  *-magma;  *-semigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid
+    )
 
   semiringWithoutOne : SemiringWithoutOne _ _
   semiringWithoutOne =
     record { isSemiringWithoutOne = isSemiringWithoutOne }
 
   open SemiringWithoutOne semiringWithoutOne public
-         using (nearSemiring)
+    using (nearSemiring)
 
 record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _*_
@@ -361,11 +390,12 @@ record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
     record { isSemiringWithoutOne = isSemiringWithoutOne }
 
   open SemiringWithoutOne semiringWithoutOne public
-         using ( +-semigroup; +-rawMonoid; +-monoid
-               ; +-commutativeMonoid
-               ; *-semigroup
-               ; nearSemiring
-               )
+    using
+    ( +-rawMagma; +-magma; +-semigroup
+    ; *-rawMagma; *-magma; *-semigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; nearSemiring
+    )
 
 record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _*_
@@ -386,13 +416,15 @@ record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
   semiring = record { isSemiring = isSemiring }
 
   open Semiring semiring public
-         using ( +-semigroup; +-rawMonoid; +-monoid
-               ; +-commutativeMonoid
-               ; *-semigroup; *-rawMonoid; *-monoid
-               ; nearSemiring; semiringWithoutOne
-               ; semiringWithoutAnnihilatingZero
-               ; rawSemiring
-               )
+    using
+    ( +-rawMagma; +-magma; +-semigroup
+    ; *-rawMagma; *-magma; *-semigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid
+    ; nearSemiring; semiringWithoutOne
+    ; semiringWithoutAnnihilatingZero
+    ; rawSemiring
+    )
 
   *-commutativeMonoid : CommutativeMonoid _ _
   *-commutativeMonoid =
@@ -444,15 +476,17 @@ record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
   semiring = record { isSemiring = isSemiring }
 
   open Semiring semiring public
-         using ( +-semigroup; +-rawMonoid; +-monoid
-               ; +-commutativeMonoid
-               ; *-semigroup; *-rawMonoid; *-monoid
-               ; nearSemiring; semiringWithoutOne
-               ; semiringWithoutAnnihilatingZero
-               )
+    using
+    ( +-rawMagma; +-magma; +-semigroup
+    ; *-rawMagma; *-magma; *-semigroup
+    ; +-rawMonoid; +-monoid ; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid
+    ; nearSemiring; semiringWithoutOne
+    ; semiringWithoutAnnihilatingZero
+    )
 
   open AbelianGroup +-abelianGroup public
-         using () renaming (group to +-group)
+    using () renaming (group to +-group)
 
   rawRing : RawRing _
   rawRing = record
@@ -489,12 +523,15 @@ record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Ring ring public using (rawRing; +-group; +-abelianGroup)
   open CommutativeSemiring commutativeSemiring public
-         using ( +-semigroup; +-rawMonoid; +-monoid; +-commutativeMonoid
-               ; *-semigroup; *-rawMonoid; *-monoid; *-commutativeMonoid
-               ; nearSemiring; semiringWithoutOne
-               ; semiringWithoutAnnihilatingZero; semiring
-               ; commutativeSemiringWithoutOne
-               )
+    using
+    ( +-rawMagma; +-magma; +-semigroup
+    ; *-rawMagma; *-magma; *-semigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid; *-commutativeMonoid
+    ; nearSemiring; semiringWithoutOne
+    ; semiringWithoutAnnihilatingZero; semiring
+    ; commutativeSemiringWithoutOne
+    )
 
 ------------------------------------------------------------------------
 -- Lattices and boolean algebras
@@ -513,7 +550,7 @@ record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
   band : Band c ℓ
   band = record { isBand = isBand }
 
-  open Band band public using (semigroup)
+  open Band band public using (rawMagma; magma; semigroup)
 
 record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 7 _∧_
@@ -572,3 +609,18 @@ record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open DistributiveLattice distributiveLattice public
          using (setoid; lattice)
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 0.18
+
+RawSemigroup = RawMagma
+{-# WARNING_ON_USAGE RawSemigroup
+"Warning: RawSemigroup was deprecated in v0.18.
+Please use RawMagma instead."
+#-}
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index 087c814821..954c1360ce 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -7,7 +7,7 @@
 
 open import Relation.Binary using (Rel; Setoid; IsEquivalence)
 
--- The structures are parameterised by the following "equality" relation
+-- The structures are parameterised by an equivalence relation
 
 module Algebra.Structures {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where
 
@@ -19,17 +19,32 @@ open import Level using (_⊔_)
 ------------------------------------------------------------------------
 -- Semigroups
 
-record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
+record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
   field
     isEquivalence : IsEquivalence _≈_
-    assoc         : Associative ∙
     ∙-cong        : Congruent₂ ∙
 
+  open IsEquivalence isEquivalence public
+
   setoid : Setoid a ℓ
   setoid = record { isEquivalence = isEquivalence }
 
+record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
+  field
+    isEquivalence : IsEquivalence _≈_
+    ∙-cong        : Congruent₂ ∙
+    assoc         : Associative ∙
+
   open IsEquivalence isEquivalence public
 
+  isMagma : IsMagma ∙
+  isMagma = record
+    { isEquivalence = isEquivalence
+    ; ∙-cong        = ∙-cong
+    }
+
+  open IsMagma isMagma public using (setoid)
+
 record IsBand (∙ : Op₂ A) : Set (a ⊔ ℓ) where
   field
     isSemigroup : IsSemigroup ∙
@@ -47,14 +62,14 @@ record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
     isSemigroup : IsSemigroup ∙
     identity    : Identity ε ∙
 
+  open IsSemigroup isSemigroup public
+
   identityˡ : LeftIdentity ε ∙
   identityˡ = proj₁ identity
 
   identityʳ : RightIdentity ε ∙
   identityʳ = proj₂ identity
 
-  open IsSemigroup isSemigroup public
-
 record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
   field
     isSemigroup : IsSemigroup ∙
@@ -141,10 +156,11 @@ record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
     renaming
     ( assoc       to +-assoc
     ; ∙-cong      to +-cong
-    ; isSemigroup to +-isSemigroup
     ; identity    to +-identity
     ; identityˡ   to +-identityˡ
     ; identityʳ   to +-identityʳ
+    ; isMagma     to +-isMagma
+    ; isSemigroup to +-isSemigroup
     )
 
   open IsSemigroup *-isSemigroup public
@@ -152,6 +168,7 @@ record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
     renaming
     ( assoc    to *-assoc
     ; ∙-cong   to *-cong
+    ; isMagma  to *-isMagma
     )
 
 record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
@@ -211,12 +228,13 @@ record IsSemiringWithoutAnnihilatingZero (+ * : Op₂ A)
     renaming
     ( assoc       to +-assoc
     ; ∙-cong      to +-cong
-    ; isSemigroup to +-isSemigroup
     ; identity    to +-identity
     ; identityˡ   to +-identityˡ
     ; identityʳ   to +-identityʳ
-    ; isMonoid    to +-isMonoid
     ; comm        to +-comm
+    ; isMagma     to +-isMagma
+    ; isSemigroup to +-isSemigroup
+    ; isMonoid    to +-isMonoid
     )
 
   open IsMonoid *-isMonoid public
@@ -224,10 +242,11 @@ record IsSemiringWithoutAnnihilatingZero (+ * : Op₂ A)
     renaming
     ( assoc       to *-assoc
     ; ∙-cong      to *-cong
-    ; isSemigroup to *-isSemigroup
     ; identity    to *-identity
     ; identityˡ   to *-identityˡ
     ; identityʳ   to *-identityʳ
+    ; isMagma     to *-isMagma
+    ; isSemigroup to *-isSemigroup
     )
 
 record IsSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
@@ -324,18 +343,19 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
     renaming
     ( assoc               to +-assoc
     ; ∙-cong              to +-cong
-    ; isSemigroup         to +-isSemigroup
     ; identity            to +-identity
     ; identityˡ           to +-identityˡ
     ; identityʳ           to +-identityʳ
-    ; isMonoid            to +-isMonoid
     ; inverse             to -‿inverse
     ; inverseˡ            to -‿inverseˡ
     ; inverseʳ            to -‿inverseʳ
     ; ⁻¹-cong             to -‿cong
-    ; isGroup             to +-isGroup
     ; comm                to +-comm
+    ; isMagma             to +-isMagma
+    ; isSemigroup         to +-isSemigroup
+    ; isMonoid            to +-isMonoid
     ; isCommutativeMonoid to +-isCommutativeMonoid
+    ; isGroup             to +-isGroup
     )
 
   open IsMonoid *-isMonoid public
@@ -343,10 +363,11 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
     renaming
     ( assoc       to *-assoc
     ; ∙-cong      to *-cong
-    ; isSemigroup to *-isSemigroup
     ; identity    to *-identity
     ; identityˡ   to *-identityˡ
     ; identityʳ   to *-identityʳ
+    ; isMagma     to *-isMagma
+    ; isSemigroup to *-isSemigroup
     )
 
   zeroˡ : LeftZero 0# *
@@ -394,8 +415,8 @@ record IsCommutativeRing
       ; identityˡ   = *-identityˡ
       ; comm        = *-comm
       }
-    ; distribʳ              = proj₂ distrib
-    ; zeroˡ                 = proj₁ zero
+    ; distribʳ              = distribʳ
+    ; zeroˡ                 = zeroˡ
     }
 
   open IsCommutativeSemiring isCommutativeSemiring public