diff --git a/src/group-theory/groups.lagda.md b/src/group-theory/groups.lagda.md
index c6df41df88..e58610be57 100644
--- a/src/group-theory/groups.lagda.md
+++ b/src/group-theory/groups.lagda.md
@@ -70,6 +70,9 @@ is-group-is-unital-Semigroup G is-unital-Semigroup-G =
       ( (x : type-Semigroup G) →
         mul-Semigroup G x (i x) ＝ pr1 is-unital-Semigroup-G))
 
+is-group-Monoid : {l : Level} → Monoid l → UU l
+is-group-Monoid = ind-Σ is-group-is-unital-Semigroup
+
 is-group-Semigroup :
   {l : Level} (G : Semigroup l) → UU l
 is-group-Semigroup G =
@@ -680,3 +683,12 @@ module _
   pr1 pointed-type-with-aut-Group = pointed-type-Group G
   pr2 pointed-type-with-aut-Group = equiv-mul-Group G g
 ```
+
+### Making groups from monoids
+
+```agda
+group-is-group-Monoid :
+  {l : Level} (M : Monoid l) → is-group-Monoid M → Group l
+group-is-group-Monoid (G , is-unital-G) is-group-G =
+  ( G , is-unital-G , is-group-G)
+```
diff --git a/src/group-theory/homomorphisms-semigroups.lagda.md b/src/group-theory/homomorphisms-semigroups.lagda.md
index 2312dc77ab..5f2abdea66 100644
--- a/src/group-theory/homomorphisms-semigroups.lagda.md
+++ b/src/group-theory/homomorphisms-semigroups.lagda.md
@@ -28,8 +28,10 @@ open import group-theory.semigroups
 
 ## Idea
 
-A homomorphism between two semigroups is a map between their underlying types
-that preserves the binary operation.
+A
+{{#concept "homomorphism" Disambiguation="between semigroups" Agda=hom-Semigroup}}
+between two [semigroups](group-theory.semigroups.md) is a map between their
+underlying types that preserves the binary operation.
 
 ## Definition
 
@@ -144,20 +146,20 @@ module _
         ( is-torsorial-htpy-hom-Semigroup f)
         ( htpy-eq-hom-Semigroup f)
 
-  eq-htpy-hom-Semigroup :
-    {f g : hom-Semigroup} → htpy-hom-Semigroup f g → f ＝ g
-  eq-htpy-hom-Semigroup {f} {g} =
-    map-inv-is-equiv (is-equiv-htpy-eq-hom-Semigroup f g)
-
-  is-set-hom-Semigroup : is-set hom-Semigroup
-  is-set-hom-Semigroup f g =
-    is-prop-is-equiv
-      ( is-equiv-htpy-eq-hom-Semigroup f g)
-      ( is-prop-Π
-        ( λ x →
-          is-set-type-Semigroup H
-            ( map-hom-Semigroup f x)
-            ( map-hom-Semigroup g x)))
+    eq-htpy-hom-Semigroup :
+      {f g : hom-Semigroup} → htpy-hom-Semigroup f g → f ＝ g
+    eq-htpy-hom-Semigroup {f} {g} =
+      map-inv-is-equiv (is-equiv-htpy-eq-hom-Semigroup f g)
+
+    is-set-hom-Semigroup : is-set hom-Semigroup
+    is-set-hom-Semigroup f g =
+      is-prop-is-equiv
+        ( is-equiv-htpy-eq-hom-Semigroup f g)
+        ( is-prop-Π
+          ( λ x →
+            is-set-type-Semigroup H
+              ( map-hom-Semigroup f x)
+              ( map-hom-Semigroup g x)))
 
   hom-set-Semigroup : Set (l1 ⊔ l2)
   pr1 hom-set-Semigroup = hom-Semigroup
diff --git a/src/universal-algebra.lagda.md b/src/universal-algebra.lagda.md
index 9f5069e870..de1eb0f30d 100644
--- a/src/universal-algebra.lagda.md
+++ b/src/universal-algebra.lagda.md
@@ -7,7 +7,11 @@ module universal-algebra where
 
 open import universal-algebra.abstract-equations-over-signatures public
 open import universal-algebra.algebraic-theories public
+open import universal-algebra.algebraic-theory-of-abelian-groups public
 open import universal-algebra.algebraic-theory-of-groups public
+open import universal-algebra.algebraic-theory-of-left-modules-rings public
+open import universal-algebra.algebraic-theory-of-monoids public
+open import universal-algebra.algebraic-theory-of-semigroups public
 open import universal-algebra.algebras public
 open import universal-algebra.category-of-algebras-algebraic-theories public
 open import universal-algebra.congruences public
diff --git a/src/universal-algebra/abstract-equations-over-signatures.lagda.md b/src/universal-algebra/abstract-equations-over-signatures.lagda.md
index 45f5d5bed0..26198f15b3 100644
--- a/src/universal-algebra/abstract-equations-over-signatures.lagda.md
+++ b/src/universal-algebra/abstract-equations-over-signatures.lagda.md
@@ -7,10 +7,13 @@ module universal-algebra.abstract-equations-over-signatures where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.natural-numbers
+
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.universe-levels
 
+open import universal-algebra.extensions-signatures
 open import universal-algebra.signatures
 open import universal-algebra.terms-over-signatures
 ```
@@ -37,11 +40,36 @@ module _
   where
 
   abstract-equation : UU l1
-  abstract-equation = term σ × term σ
+  abstract-equation = Σ ℕ (λ k → term σ k × term σ k)
+
+module _
+  {l : Level} (σ : signature l) ((k , lhs , rhs) : abstract-equation σ)
+  where
 
-  lhs-abstract-equation : abstract-equation → term σ
-  lhs-abstract-equation = pr1
+  arity-abstract-equation : ℕ
+  arity-abstract-equation = k
+
+  lhs-abstract-equation : term σ arity-abstract-equation
+  lhs-abstract-equation = lhs
+
+  rhs-abstract-equation : term σ arity-abstract-equation
+  rhs-abstract-equation = rhs
+```
+
+## Properties
+
+### Translation of equations
+
+```agda
+module _
+  {l1 l2 : Level}
+  (σ : signature l1)
+  (τ : signature l2)
+  (E : is-extension-of-signature σ τ)
+  where
 
-  rhs-abstract-equation : abstract-equation → term σ
-  rhs-abstract-equation = pr2
+  translation-abstract-equation :
+    abstract-equation σ → abstract-equation τ
+  translation-abstract-equation (k , lhs , rhs) =
+    ( k , translation-term σ τ E lhs , translation-term σ τ E rhs)
 ```
diff --git a/src/universal-algebra/algebraic-theory-of-abelian-groups.lagda.md b/src/universal-algebra/algebraic-theory-of-abelian-groups.lagda.md
new file mode 100644
index 0000000000..159425e4a8
--- /dev/null
+++ b/src/universal-algebra/algebraic-theory-of-abelian-groups.lagda.md
@@ -0,0 +1,212 @@
+# The algebraic theory of abelian groups
+
+```agda
+module universal-algebra.algebraic-theory-of-abelian-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.binary-homotopies
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+open import group-theory.groups
+open import group-theory.homomorphisms-abelian-groups
+
+open import lists.tuples
+
+open import univalent-combinatorics.standard-finite-types
+
+open import universal-algebra.algebraic-theories
+open import universal-algebra.algebraic-theory-of-groups
+open import universal-algebra.algebras
+open import universal-algebra.homomorphisms-of-algebras
+open import universal-algebra.models-of-signatures
+open import universal-algebra.signatures
+open import universal-algebra.terms-over-signatures
+```
+
+</details>
+
+## Idea
+
+There is an
+{{#concept "algebraic theory of abelian groups" Agda=algebraic-theory-Ab}}. The
+type of all such [algebras](universal-algebra.algebras.md) is
+[equivalent](foundation-core.equivalences.md) to the type of
+[abelian groups](group-theory.abelian-groups.md).
+
+## Definition
+
+```agda
+operation-Ab : UU lzero
+operation-Ab = operation-Group
+
+pattern zero-operation-Ab = unit-operation-Group
+pattern add-operation-Ab = mul-operation-Group
+pattern neg-operation-Ab = inv-operation-Group
+
+signature-Ab : signature lzero
+signature-Ab = signature-Group
+
+data law-Ab : UU lzero where
+  law-ab-law-Group : law-Group → law-Ab
+  commutative-add-law-Ab : law-Ab
+
+pattern associative-add-law-Ab = law-ab-law-Group associative-mul-law-Group
+pattern left-unit-add-law-Ab = law-ab-law-Group left-unit-mul-law-Group
+pattern right-unit-add-law-Ab = law-ab-law-Group right-unit-mul-law-Group
+pattern left-inverse-add-law-Ab = law-ab-law-Group left-inverse-mul-law-Group
+pattern right-inverse-add-law-Ab = law-ab-law-Group right-inverse-mul-law-Group
+
+algebraic-theory-Ab : Algebraic-Theory lzero signature-Ab
+pr1 algebraic-theory-Ab = law-Ab
+pr2 algebraic-theory-Ab (law-ab-law-Group law) =
+  index-abstract-equation-Algebraic-Theory
+    ( signature-Group)
+    ( algebraic-theory-Group)
+    ( law)
+pr2 algebraic-theory-Ab commutative-add-law-Ab =
+  let
+    x-term = var-term (zero-Fin 1)
+    y-term = var-term (one-Fin 1)
+    add-term x y = op-term add-operation-Ab (x ∷ y ∷ empty-tuple)
+  in
+    ( 2 ,
+      add-term x-term y-term ,
+      add-term y-term x-term)
+
+Algebra-Ab : (l : Level) → UU (lsuc l)
+Algebra-Ab l = Algebra l signature-Ab algebraic-theory-Ab
+```
+
+## Properties
+
+### Algebras in the theory of abelian groups from abelian groups
+
+```agda
+module _
+  {l : Level}
+  (G : Ab l)
+  where
+
+  algebra-group-Ab : Algebra-Group l
+  algebra-group-Ab = algebra-group-Group (group-Ab G)
+
+  model-set-Ab : Model-Of-Signature l signature-Ab
+  model-set-Ab = model-set-Group (group-Ab G)
+
+  is-algebra-model-set-Ab :
+    is-algebra-Model-of-Signature
+      ( signature-Ab)
+      ( algebraic-theory-Ab)
+      ( model-set-Ab)
+  is-algebra-model-set-Ab (law-ab-law-Group law) =
+    is-algebra-model-set-Group (group-Ab G) law
+  is-algebra-model-set-Ab commutative-add-law-Ab _ = commutative-add-Ab G _ _
+
+  algebra-ab-Ab : Algebra-Ab l
+  algebra-ab-Ab = (model-set-Ab , is-algebra-model-set-Ab)
+```
+
+### Abelian groups from algebras in the theory of abelian groups
+
+```agda
+module _
+  {l : Level}
+  (A@((set-A , model-A) , satisfies-A) : Algebra-Ab l)
+  where
+
+  algebra-group-Algebra-Ab : Algebra-Group l
+  algebra-group-Algebra-Ab =
+    ((set-A , model-A) , satisfies-A ∘ law-ab-law-Group)
+
+  group-Algebra-Ab : Group l
+  group-Algebra-Ab = group-Algebra-Group algebra-group-Algebra-Ab
+
+  type-Algebra-Ab : UU l
+  type-Algebra-Ab = type-Set set-A
+
+  add-Algebra-Ab : type-Algebra-Ab → type-Algebra-Ab → type-Algebra-Ab
+  add-Algebra-Ab = mul-Group group-Algebra-Ab
+
+  commutative-add-Algebra-Ab :
+    (x y : type-Algebra-Ab) → add-Algebra-Ab x y ＝ add-Algebra-Ab y x
+  commutative-add-Algebra-Ab x y =
+    satisfies-A commutative-add-law-Ab (component-tuple 2 (y ∷ x ∷ empty-tuple))
+
+  ab-Algebra-Ab : Ab l
+  ab-Algebra-Ab = (group-Algebra-Ab , commutative-add-Algebra-Ab)
+```
+
+### The type of abelian groups is equivalent to the type of algebras in the algebraic theory of abelian groups
+
+```agda
+abstract
+  is-section-ab-Algebra-Ab :
+    {l : Level} (A : Algebra-Ab l) → algebra-ab-Ab (ab-Algebra-Ab A) ＝ A
+  is-section-ab-Algebra-Ab A =
+    eq-type-subtype
+      ( is-algebra-prop-Model-Of-Signature
+        ( signature-Ab)
+        ( algebraic-theory-Ab))
+      ( ap
+        ( model-Algebra signature-Group algebraic-theory-Group)
+        ( is-section-group-Algebra-Group (algebra-group-Algebra-Ab A)))
+
+  is-retraction-ab-Algebra-Ab :
+    {l : Level} (G : Ab l) → ab-Algebra-Ab (algebra-ab-Ab G) ＝ G
+  is-retraction-ab-Algebra-Ab _ = refl
+
+is-equiv-algebra-ab-Ab :
+  {l : Level} → is-equiv (algebra-ab-Ab {l})
+is-equiv-algebra-ab-Ab =
+  is-equiv-is-invertible
+    ( ab-Algebra-Ab)
+    ( is-section-ab-Algebra-Ab)
+    ( is-retraction-ab-Algebra-Ab)
+
+equiv-ab-Algebra-Ab :
+  {l : Level} → Ab l ≃ Algebra-Ab l
+equiv-ab-Algebra-Ab = (algebra-ab-Ab , is-equiv-algebra-ab-Ab)
+```
+
+### Homomorphisms of abelian groups are equivalent to homomorphisms of algebras in the theory of abelian groups
+
+```agda
+hom-Algebra-Ab : {l1 l2 : Level} → Algebra-Ab l1 → Algebra-Ab l2 → UU (l1 ⊔ l2)
+hom-Algebra-Ab = hom-Algebra signature-Ab algebraic-theory-Ab
+
+hom-ab-hom-Algebra-Ab :
+  {l1 l2 : Level} (G : Algebra-Ab l1) (H : Algebra-Ab l2) →
+  hom-Algebra-Ab G H → hom-Ab (ab-Algebra-Ab G) (ab-Algebra-Ab H)
+hom-ab-hom-Algebra-Ab G H =
+  hom-group-hom-Algebra-Group
+    ( algebra-group-Algebra-Ab G)
+    ( algebra-group-Algebra-Ab H)
+
+module _
+  {l1 l2 : Level}
+  (G : Ab l1)
+  (H : Ab l2)
+  where
+
+  equiv-hom-ab-hom-Algebra-Ab :
+    hom-Ab G H ≃ hom-Algebra-Ab (algebra-ab-Ab G) (algebra-ab-Ab H)
+  equiv-hom-ab-hom-Algebra-Ab =
+    equiv-hom-group-hom-Algebra-Group (group-Ab G) (group-Ab H)
+
+  hom-algebra-ab-hom-Ab :
+    hom-Ab G H → hom-Algebra-Ab (algebra-ab-Ab G) (algebra-ab-Ab H)
+  hom-algebra-ab-hom-Ab = map-equiv equiv-hom-ab-hom-Algebra-Ab
+```
diff --git a/src/universal-algebra/algebraic-theory-of-groups.lagda.md b/src/universal-algebra/algebraic-theory-of-groups.lagda.md
index f33db75c36..4c75a89a78 100644
--- a/src/universal-algebra/algebraic-theory-of-groups.lagda.md
+++ b/src/universal-algebra/algebraic-theory-of-groups.lagda.md
@@ -7,24 +7,32 @@ module universal-algebra.algebraic-theory-of-groups where
 <details><summary>Imports</summary>
 
 ```agda
-open import elementary-number-theory.natural-numbers
-
+open import foundation.binary-homotopies
 open import foundation.dependent-pair-types
 open import foundation.equality-dependent-pair-types
 open import foundation.equivalences
-open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.homotopies
 open import foundation.identity-types
-open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
 open import foundation.universe-levels
 
 open import group-theory.groups
 open import group-theory.homomorphisms-groups
+open import group-theory.monoids
 
 open import lists.tuples
 
+open import univalent-combinatorics.standard-finite-types
+
+open import universal-algebra.abstract-equations-over-signatures
 open import universal-algebra.algebraic-theories
+open import universal-algebra.algebraic-theory-of-monoids
 open import universal-algebra.algebras
+open import universal-algebra.extensions-signatures
 open import universal-algebra.homomorphisms-of-algebras
+open import universal-algebra.models-of-signatures
 open import universal-algebra.signatures
 open import universal-algebra.terms-over-signatures
 ```
@@ -44,149 +52,259 @@ of all such [algebras](universal-algebra.algebras.md) is
 ### The algebra of groups
 
 ```agda
-data group-ops : UU lzero where
-  unit-group-op mul-group-op inv-group-op : group-ops
-
-group-signature : signature lzero
-pr1 group-signature = group-ops
-pr2 group-signature unit-group-op = 0
-pr2 group-signature mul-group-op = 2
-pr2 group-signature inv-group-op = 1
-
-data group-laws : UU lzero where
-  associative-l-group-laws : group-laws
-  invl-l-group-laws : group-laws
-  invr-r-group-laws : group-laws
-  idl-l-group-laws : group-laws
-  idr-r-group-laws : group-laws
-
-algebraic-theory-Group : Algebraic-Theory lzero group-signature
-pr1 algebraic-theory-Group = group-laws
+data operation-Group : UU lzero where
+  operation-group-operation-Monoid : operation-Monoid → operation-Group
+  inv-operation-Group : operation-Group
+
+pattern mul-operation-Group =
+  operation-group-operation-Monoid mul-operation-Monoid
+pattern unit-operation-Group =
+  operation-group-operation-Monoid unit-operation-Monoid
+
+signature-Group : signature lzero
+pr1 signature-Group = operation-Group
+pr2 signature-Group (operation-group-operation-Monoid op) =
+  arity-operation-signature signature-Monoid op
+pr2 signature-Group inv-operation-Group = 1
+
+data law-Group : UU lzero where
+  law-group-law-Monoid : law-Monoid → law-Group
+  left-inverse-mul-law-Group : law-Group
+  right-inverse-mul-law-Group : law-Group
+
+pattern associative-mul-law-Group =
+  law-group-law-Monoid associative-mul-law-Monoid
+pattern left-unit-mul-law-Group =
+  law-group-law-Monoid left-unit-mul-law-Monoid
+pattern right-unit-mul-law-Group =
+  law-group-law-Monoid right-unit-mul-law-Monoid
+
+extension-signature-monoid-Group :
+  is-extension-of-signature signature-Monoid signature-Group
+pr1 extension-signature-monoid-Group =
+  operation-group-operation-Monoid
+pr2 extension-signature-monoid-Group _ = refl
+
+algebraic-theory-Group : Algebraic-Theory lzero signature-Group
+pr1 algebraic-theory-Group = law-Group
 pr2 algebraic-theory-Group =
-  λ where
-  associative-l-group-laws →
-    ( op mul-group-op
-      ( ( op mul-group-op (var 0 ∷ var 1 ∷ empty-tuple)) ∷
-        var 2 ∷
-        empty-tuple)) ,
-    ( op mul-group-op
-      ( var 0 ∷ (op mul-group-op (var 1 ∷ var 2 ∷ empty-tuple)) ∷ empty-tuple))
-  invl-l-group-laws →
-    ( op mul-group-op
-      ( op inv-group-op (var 0 ∷ empty-tuple) ∷ var 0 ∷ empty-tuple)) ,
-    ( op unit-group-op empty-tuple)
-  invr-r-group-laws →
-    ( op mul-group-op
-      ( var 0 ∷ op inv-group-op (var 0 ∷ empty-tuple) ∷ empty-tuple)) ,
-    ( op unit-group-op empty-tuple)
-  idl-l-group-laws →
-    ( op mul-group-op (op unit-group-op empty-tuple ∷ var 0 ∷ empty-tuple)) ,
-    ( var 0)
-  idr-r-group-laws →
-    ( op mul-group-op (var 0 ∷ op unit-group-op empty-tuple ∷ empty-tuple)) ,
-    ( var 0)
-    where
-    op = op-term
-    var = var-term
-
-algebra-Group : (l : Level) → UU (lsuc l)
-algebra-Group l = Algebra l group-signature algebraic-theory-Group
+  let
+    var = var-term (zero-Fin 0)
+    _*-term_ x y = op-term mul-operation-Group (x ∷ y ∷ empty-tuple)
+    inv-term x = op-term inv-operation-Group (x ∷ empty-tuple)
+    unit-term = op-term unit-operation-Group empty-tuple
+  in
+    λ where
+      (law-group-law-Monoid law) →
+        translation-abstract-equation
+          ( signature-Monoid)
+          ( signature-Group)
+          ( extension-signature-monoid-Group)
+          ( index-abstract-equation-Algebraic-Theory
+            ( signature-Monoid)
+            ( algebraic-theory-Monoid)
+            ( law))
+      left-inverse-mul-law-Group →
+        ( 1 ,
+          inv-term var *-term var ,
+          unit-term)
+      right-inverse-mul-law-Group →
+        ( 1 ,
+          var *-term inv-term var ,
+          unit-term)
+
+Algebra-Group : (l : Level) → UU (lsuc l)
+Algebra-Group l = Algebra l signature-Group algebraic-theory-Group
 ```
 
 ## Properties
 
-### The algebra of groups is equivalent to the type of groups
+### Algebras in the theory of groups from groups
 
 ```agda
-group-algebra-Group :
-  {l : Level} → algebra-Group l → Group l
-pr1 (pr1 (group-algebra-Group ((A-Set , models-A) , satisfies-A))) = A-Set
-pr1 (pr2 (pr1 (group-algebra-Group ((A-Set , models-A) , satisfies-A)))) x y =
-  models-A mul-group-op (x ∷ y ∷ empty-tuple)
-pr2 (pr2 (pr1 (group-algebra-Group ((A-Set , models-A) , satisfies-A)))) x y z =
-  satisfies-A associative-l-group-laws
-    ( λ { 0 → x ; 1 → y ; (succ-ℕ (succ-ℕ n)) → z})
-pr1 (pr1 (pr2 (group-algebra-Group ((A-Set , models-A) , satisfies-A)))) =
-  models-A unit-group-op empty-tuple
-pr1 (pr2 (pr1 (pr2 (group-algebra-Group (_ , satisfies-A))))) x =
-  satisfies-A idl-l-group-laws (λ _ → x)
-pr2 (pr2 (pr1 (pr2 (group-algebra-Group (_ , satisfies-A))))) x =
-  satisfies-A idr-r-group-laws (λ _ → x)
-pr1 (pr2 (pr2 (group-algebra-Group ((A-Set , models-A) , satisfies-A)))) x =
-  models-A inv-group-op (x ∷ empty-tuple)
-pr1 (pr2 (pr2 (pr2 (group-algebra-Group (_ , satisfies-A))))) x =
-  satisfies-A invl-l-group-laws (λ _ → x)
-pr2 (pr2 (pr2 (pr2 (group-algebra-Group (_ , satisfies-A))))) x =
-  satisfies-A invr-r-group-laws (λ _ → x)
-
-algebra-group-Group :
-  {l : Level} → Group l → algebra-Group l
-algebra-group-Group G =
-  pair
-    ( pair
-      ( set-Group G)
-      ( λ where
-        unit-group-op v → unit-Group G
-        mul-group-op (x ∷ y ∷ empty-tuple) → mul-Group G x y
-        inv-group-op (x ∷ empty-tuple) → inv-Group G x))
-    ( λ where
-      associative-l-group-laws assign →
-        associative-mul-Group G (assign 0) (assign 1) (assign 2)
-      invl-l-group-laws assign →
-        left-inverse-law-mul-Group G (assign 0)
-      invr-r-group-laws assign →
-        right-inverse-law-mul-Group G (assign 0)
-      idl-l-group-laws assign →
-        left-unit-law-mul-Group G (assign 0)
-      idr-r-group-laws assign →
-        right-unit-law-mul-Group G (assign 0))
+module _
+  {l : Level}
+  (G : Group l)
+  where
+
+  algebra-monoid-Group : Algebra-Monoid l
+  algebra-monoid-Group =
+    algebra-monoid-Monoid (monoid-Group G)
+
+  is-model-set-Group : is-model-of-signature signature-Group (set-Group G)
+  is-model-set-Group (operation-group-operation-Monoid op) =
+    is-model-set-Monoid (monoid-Group G) op
+  is-model-set-Group inv-operation-Group (x ∷ empty-tuple) =
+    inv-Group G x
+
+  model-set-Group : Model-Of-Signature l signature-Group
+  model-set-Group = (set-Group G , is-model-set-Group)
+
+  is-algebra-model-set-Group :
+    is-algebra-Model-of-Signature
+      ( signature-Group)
+      ( algebraic-theory-Group)
+      ( model-set-Group)
+  is-algebra-model-set-Group associative-mul-law-Group _ =
+    associative-mul-Group G _ _ _
+  is-algebra-model-set-Group left-unit-mul-law-Group _ =
+    left-unit-law-mul-Group G _
+  is-algebra-model-set-Group right-unit-mul-law-Group _ =
+    right-unit-law-mul-Group G _
+  is-algebra-model-set-Group left-inverse-mul-law-Group _ =
+    left-inverse-law-mul-Group G _
+  is-algebra-model-set-Group right-inverse-mul-law-Group _ =
+    right-inverse-law-mul-Group G _
+
+  algebra-group-Group : Algebra-Group l
+  algebra-group-Group = (model-set-Group , is-algebra-model-set-Group)
+```
+
+### Groups from algebras in the theory of groups
+
+```agda
+module _
+  {l : Level}
+  (A@((set-A , model-A) , satisfies-A) : Algebra-Group l)
+  where
+
+  algebra-monoid-Algebra-Group : Algebra-Monoid l
+  algebra-monoid-Algebra-Group =
+    ( ( set-A , model-A ∘ operation-group-operation-Monoid) ,
+      λ where
+        associative-mul-law-Monoid → satisfies-A associative-mul-law-Group
+        left-unit-mul-law-Monoid → satisfies-A left-unit-mul-law-Group
+        right-unit-mul-law-Monoid → satisfies-A right-unit-mul-law-Group)
 
+  monoid-Algebra-Group : Monoid l
+  monoid-Algebra-Group = monoid-Algebra-Monoid algebra-monoid-Algebra-Group
+
+  type-Algebra-Group : UU l
+  type-Algebra-Group = type-Set set-A
+
+  mul-Algebra-Group :
+    type-Algebra-Group → type-Algebra-Group → type-Algebra-Group
+  mul-Algebra-Group = mul-Monoid monoid-Algebra-Group
+
+  unit-Algebra-Group : type-Algebra-Group
+  unit-Algebra-Group = unit-Monoid monoid-Algebra-Group
+
+  inv-Algebra-Group : type-Algebra-Group → type-Algebra-Group
+  inv-Algebra-Group x = model-A inv-operation-Group (x ∷ empty-tuple)
+
+  left-inverse-law-mul-Algebra-Group :
+    (x : type-Algebra-Group) →
+    mul-Algebra-Group (inv-Algebra-Group x) x ＝ unit-Algebra-Group
+  left-inverse-law-mul-Algebra-Group x =
+    satisfies-A left-inverse-mul-law-Group (λ _ → x)
+
+  right-inverse-law-mul-Algebra-Group :
+    (x : type-Algebra-Group) →
+    mul-Algebra-Group x (inv-Algebra-Group x) ＝ unit-Algebra-Group
+  right-inverse-law-mul-Algebra-Group x =
+    satisfies-A right-inverse-mul-law-Group (λ _ → x)
+
+  group-Algebra-Group : Group l
+  group-Algebra-Group =
+    group-is-group-Monoid
+      ( monoid-Algebra-Group)
+      ( inv-Algebra-Group ,
+        left-inverse-law-mul-Algebra-Group ,
+        right-inverse-law-mul-Algebra-Group)
+```
+
+### The type of groups is equivalent to the type of algebras in the theory of groups
+
+```agda
 abstract
-  equiv-group-algebra-Group :
-    {l : Level} → algebra-Group l ≃ Group l
-  pr1 equiv-group-algebra-Group = group-algebra-Group
-  pr1 (pr1 (pr2 equiv-group-algebra-Group)) = algebra-group-Group
-  pr2 (pr1 (pr2 equiv-group-algebra-Group)) G =
-    eq-pair-eq-fiber
-      ( eq-is-prop (is-prop-is-group-Semigroup (semigroup-Group G)))
-  pr1 (pr2 (pr2 equiv-group-algebra-Group)) = algebra-group-Group
-  pr2 (pr2 (pr2 equiv-group-algebra-Group)) A =
-    eq-pair-Σ
+  is-section-group-Algebra-Group :
+    {l : Level} (A : Algebra-Group l) →
+    algebra-group-Group (group-Algebra-Group A) ＝ A
+  is-section-group-Algebra-Group ((set-A , models-A) , satisfies-A) =
+    eq-type-subtype
+      ( is-algebra-prop-Model-Of-Signature
+        ( signature-Group)
+        ( algebraic-theory-Group))
       ( eq-pair-eq-fiber
-        ( eq-htpy
+        ( eq-binary-htpy _ _
           ( λ where
-            unit-group-op → eq-htpy (λ where empty-tuple → refl)
-            mul-group-op → eq-htpy (λ where (x ∷ y ∷ empty-tuple) → refl)
-            inv-group-op → eq-htpy (λ where (x ∷ empty-tuple) → refl))))
-      ( eq-is-prop
-        ( is-prop-is-algebra
-          ( group-signature) ( algebraic-theory-Group)
-          ( model-Algebra group-signature algebraic-theory-Group A)))
+            mul-operation-Group (x ∷ y ∷ empty-tuple) → refl
+            unit-operation-Group empty-tuple → refl
+            inv-operation-Group (x ∷ empty-tuple) → refl)))
+
+  is-retraction-group-Algebra-Group :
+    {l : Level} (G : Group l) →
+    group-Algebra-Group (algebra-group-Group G) ＝ G
+  is-retraction-group-Algebra-Group _ = refl
+
+is-equiv-algebra-group-Group :
+  {l : Level} → is-equiv (algebra-group-Group {l})
+is-equiv-algebra-group-Group =
+  is-equiv-is-invertible
+    ( group-Algebra-Group)
+    ( is-section-group-Algebra-Group)
+    ( is-retraction-group-Algebra-Group)
+
+equiv-group-Algebra-Group :
+  {l : Level} → Group l ≃ Algebra-Group l
+equiv-group-Algebra-Group =
+  ( algebra-group-Group ,
+    is-equiv-algebra-group-Group)
 ```
 
-### Homomorphisms of groups are homomorphisms of the algebra of groups, and vice versa
+### Homomorphisms of groups are equivalent to homomorphisms of algebras in the theory of groups
 
 ```agda
-hom-algebra-Group :
-  {l1 l2 : Level} → algebra-Group l1 → algebra-Group l2 → UU (l1 ⊔ l2)
-hom-algebra-Group =
-  hom-Algebra group-signature algebraic-theory-Group
-
-hom-group-hom-algebra-Group :
-  {l1 l2 : Level} (G : algebra-Group l1) (H : algebra-Group l2) →
-  hom-algebra-Group G H →
-  hom-Group (group-algebra-Group G) (group-algebra-Group H)
-hom-group-hom-algebra-Group G H (f , K) =
-  ( f , λ {x} {y} → K mul-group-op (x ∷ y ∷ empty-tuple))
-
-hom-algebra-group-hom-Group :
-  {l1 l2 : Level} (G : Group l1) (H : Group l2) →
-  hom-Group G H →
-  hom-algebra-Group (algebra-group-Group G) (algebra-group-Group H)
-hom-algebra-group-hom-Group G H (f , K) =
-  ( f ,
-    λ where
-      unit-group-op empty-tuple → preserves-unit-hom-Group G H (f , K)
-      mul-group-op (x ∷ y ∷ empty-tuple) → K {x} {y}
-      inv-group-op (x ∷ empty-tuple) → preserves-inv-hom-Group G H (f , K))
+hom-Algebra-Group :
+  {l1 l2 : Level} → Algebra-Group l1 → Algebra-Group l2 → UU (l1 ⊔ l2)
+hom-Algebra-Group = hom-Algebra signature-Group algebraic-theory-Group
+
+hom-group-hom-Algebra-Group :
+  {l1 l2 : Level} (G : Algebra-Group l1) (H : Algebra-Group l2) →
+  hom-Algebra-Group G H →
+  hom-Group (group-Algebra-Group G) (group-Algebra-Group H)
+hom-group-hom-Algebra-Group G H (φ , preserves-ops-φ) =
+  ( φ , preserves-ops-φ mul-operation-Group (_ ∷ _ ∷ empty-tuple))
+
+module _
+  {l1 l2 : Level}
+  (G : Group l1)
+  (H : Group l2)
+  where
+
+  hom-algebra-group-hom-Group :
+    hom-Group G H →
+    hom-Algebra-Group (algebra-group-Group G) (algebra-group-Group H)
+  hom-algebra-group-hom-Group hom-φ@(φ , preserves-mul-φ) =
+    ( φ ,
+      λ where
+        mul-operation-Group (x ∷ y ∷ empty-tuple) → preserves-mul-φ
+        unit-operation-Group empty-tuple → preserves-unit-hom-Group G H hom-φ
+        inv-operation-Group (x ∷ empty-tuple) →
+          preserves-inv-hom-Group G H hom-φ)
+
+  is-equiv-hom-algebra-group-hom-Group :
+    is-equiv hom-algebra-group-hom-Group
+  is-equiv-hom-algebra-group-hom-Group =
+    is-equiv-is-invertible
+      ( hom-group-hom-Algebra-Group
+        ( algebra-group-Group G)
+        ( algebra-group-Group H))
+      ( λ φ →
+        eq-htpy-hom-Algebra
+          ( signature-Group)
+          ( algebraic-theory-Group)
+          ( algebra-group-Group G)
+          ( algebra-group-Group H)
+          ( _)
+          ( φ)
+          ( refl-htpy))
+      ( λ φ → eq-htpy-hom-Group G H refl-htpy)
+
+  equiv-hom-group-hom-Algebra-Group :
+    hom-Group G H ≃
+    hom-Algebra-Group (algebra-group-Group G) (algebra-group-Group H)
+  equiv-hom-group-hom-Algebra-Group =
+    ( hom-algebra-group-hom-Group ,
+      is-equiv-hom-algebra-group-hom-Group)
 ```
diff --git a/src/universal-algebra/algebraic-theory-of-left-modules-rings.lagda.md b/src/universal-algebra/algebraic-theory-of-left-modules-rings.lagda.md
new file mode 100644
index 0000000000..710e2cc20c
--- /dev/null
+++ b/src/universal-algebra/algebraic-theory-of-left-modules-rings.lagda.md
@@ -0,0 +1,488 @@
+# The algebraic theory of left modules over rings
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module universal-algebra.algebraic-theory-of-left-modules-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.modular-arithmetic-standard-finite-types
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-homotopies
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+open import group-theory.endomorphism-rings-abelian-groups
+open import group-theory.homomorphisms-abelian-groups
+
+open import linear-algebra.left-modules-rings
+open import linear-algebra.linear-maps-left-modules-rings
+
+open import lists.tuples
+
+open import ring-theory.homomorphisms-rings
+open import ring-theory.rings
+
+open import univalent-combinatorics.standard-finite-types
+
+open import universal-algebra.abstract-equations-over-signatures
+open import universal-algebra.algebraic-theories
+open import universal-algebra.algebraic-theory-of-abelian-groups
+open import universal-algebra.algebras
+open import universal-algebra.extensions-signatures
+open import universal-algebra.homomorphisms-of-algebras
+open import universal-algebra.models-of-signatures
+open import universal-algebra.signatures
+open import universal-algebra.terms-over-signatures
+```
+
+</details>
+
+## Idea
+
+There is an
+{{#concept "algebraic theory of left modules" Agda=algebraic-theory-left-module-Ring}}
+over any [ring](ring-theory.rings.md).
+
+The type of all such [algebras](universal-algebra.algebras.md) is
+[equivalent](foundation-core.equivalences.md) to the type of
+[left modules over the ring](linear-algebra.left-modules-rings.md).
+
+## Definition
+
+```agda
+module _
+  {l : Level}
+  (R : Ring l)
+  where
+
+  data operation-left-module-Ring : UU l where
+    operation-left-module-ring-operation-Ab :
+      operation-Ab → operation-left-module-Ring
+    mul-operation-left-module-Ring :
+      type-Ring R → operation-left-module-Ring
+
+  pattern zero-operation-left-module-Ring =
+    operation-left-module-ring-operation-Ab zero-operation-Ab
+  pattern add-operation-left-module-Ring =
+    operation-left-module-ring-operation-Ab add-operation-Ab
+  pattern neg-operation-left-module-Ring =
+    operation-left-module-ring-operation-Ab neg-operation-Ab
+
+  signature-left-module-Ring : signature l
+  pr1 signature-left-module-Ring = operation-left-module-Ring
+  pr2 signature-left-module-Ring
+    ( operation-left-module-ring-operation-Ab op) =
+    arity-operation-signature signature-Ab op
+  pr2 signature-left-module-Ring (mul-operation-left-module-Ring _) = 1
+
+  data law-left-module-Ring : UU l where
+    law-left-module-ring-law-Ab : law-Ab → law-left-module-Ring
+    left-distributive-mul-add-law-left-module-Ring :
+      type-Ring R → law-left-module-Ring
+    right-distributive-mul-add-law-left-module-Ring :
+      type-Ring R → type-Ring R → law-left-module-Ring
+    left-unit-mul-law-left-module-Ring : law-left-module-Ring
+    associative-mul-law-left-module-Ring :
+      type-Ring R → type-Ring R → law-left-module-Ring
+
+  pattern associative-add-law-left-module-Ring =
+    law-left-module-ring-law-Ab associative-add-law-Ab
+  pattern left-unit-add-law-left-module-Ring =
+    law-left-module-ring-law-Ab left-unit-add-law-Ab
+  pattern right-unit-add-law-left-module-Ring =
+    law-left-module-ring-law-Ab right-unit-add-law-Ab
+  pattern left-inverse-add-law-left-module-Ring =
+    law-left-module-ring-law-Ab left-inverse-add-law-Ab
+  pattern right-inverse-add-law-left-module-Ring =
+    law-left-module-ring-law-Ab right-inverse-add-law-Ab
+  pattern commutative-add-law-left-module-Ring =
+    law-left-module-ring-law-Ab commutative-add-law-Ab
+
+  extension-signature-ab-left-module-Ring :
+    is-extension-of-signature signature-Ab signature-left-module-Ring
+  pr1 extension-signature-ab-left-module-Ring =
+    operation-left-module-ring-operation-Ab
+  pr2 extension-signature-ab-left-module-Ring _ = refl
+
+  algebraic-theory-left-module-Ring :
+    Algebraic-Theory l signature-left-module-Ring
+  pr1 algebraic-theory-left-module-Ring = law-left-module-Ring
+  pr2 algebraic-theory-left-module-Ring =
+    let
+      var : (i k : ℕ) → term signature-left-module-Ring (succ-ℕ k)
+      var i k = var-term (mod-succ-ℕ k i)
+      add-term :
+        {k : ℕ} →
+        term signature-left-module-Ring k →
+        term signature-left-module-Ring k →
+        term signature-left-module-Ring k
+      add-term x y =
+        op-term add-operation-left-module-Ring (x ∷ y ∷ empty-tuple)
+      mul-term :
+        {k : ℕ} →
+        type-Ring R → term signature-left-module-Ring k →
+        term signature-left-module-Ring k
+      mul-term r x =
+        op-term (mul-operation-left-module-Ring r) (x ∷ empty-tuple)
+    in
+      λ where
+        ( law-left-module-ring-law-Ab law) →
+          translation-abstract-equation
+            ( signature-Ab)
+            ( signature-left-module-Ring)
+            ( extension-signature-ab-left-module-Ring)
+            ( index-abstract-equation-Algebraic-Theory
+              ( signature-Ab)
+              ( algebraic-theory-Ab)
+              ( law))
+        ( left-distributive-mul-add-law-left-module-Ring r) →
+          ( 2 ,
+            mul-term r (add-term (var 0 1) (var 1 1)) ,
+            add-term (mul-term r (var 0 1)) (mul-term r (var 1 1)))
+        ( right-distributive-mul-add-law-left-module-Ring r s) →
+          ( 1 ,
+            mul-term (add-Ring R r s) (var 0 0) ,
+            add-term (mul-term r (var 0 0)) (mul-term s (var 0 0)))
+        left-unit-mul-law-left-module-Ring →
+          ( 1 ,
+            mul-term (one-Ring R) (var 0 0) ,
+            var 0 0)
+        ( associative-mul-law-left-module-Ring r s) →
+          ( 1 ,
+            mul-term (mul-Ring R r s) (var 0 0) ,
+            mul-term r (mul-term s (var 0 0)))
+
+Algebra-Left-Module-Ring :
+  {l1 : Level} (l2 : Level) → Ring l1 → UU (l1 ⊔ lsuc l2)
+Algebra-Left-Module-Ring l2 R =
+  Algebra
+    ( l2)
+    ( signature-left-module-Ring R)
+    ( algebraic-theory-left-module-Ring R)
+```
+
+## Properties
+
+### Left modules from algebras in the theory of left modules of rings
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Ring l1)
+  (A@((set-A , model-A) , satisfies-A) : Algebra-Left-Module-Ring l2 R)
+  where
+
+  algebra-ab-Algebra-Left-Module-Ring : Algebra-Ab l2
+  algebra-ab-Algebra-Left-Module-Ring =
+    ( ( set-A , model-A ∘ operation-left-module-ring-operation-Ab) ,
+      λ where
+        left-inverse-add-law-Ab →
+          satisfies-A left-inverse-add-law-left-module-Ring
+        right-inverse-add-law-Ab →
+          satisfies-A right-inverse-add-law-left-module-Ring
+        left-unit-add-law-Ab →
+          satisfies-A left-unit-add-law-left-module-Ring
+        right-unit-add-law-Ab →
+          satisfies-A right-unit-add-law-left-module-Ring
+        associative-add-law-Ab →
+          satisfies-A associative-add-law-left-module-Ring
+        commutative-add-law-Ab →
+          satisfies-A commutative-add-law-left-module-Ring)
+
+  ab-Algebra-Left-Module-Ring : Ab l2
+  ab-Algebra-Left-Module-Ring =
+    ab-Algebra-Ab algebra-ab-Algebra-Left-Module-Ring
+
+  type-Algebra-Left-Module-Ring : UU l2
+  type-Algebra-Left-Module-Ring = type-Set set-A
+
+  add-Algebra-Left-Module-Ring :
+    type-Algebra-Left-Module-Ring → type-Algebra-Left-Module-Ring →
+    type-Algebra-Left-Module-Ring
+  add-Algebra-Left-Module-Ring = add-Ab ab-Algebra-Left-Module-Ring
+
+  mul-Algebra-Left-Module-Ring :
+    type-Ring R → type-Algebra-Left-Module-Ring → type-Algebra-Left-Module-Ring
+  mul-Algebra-Left-Module-Ring r x =
+    model-A (mul-operation-left-module-Ring r) (x ∷ empty-tuple)
+
+  left-distributive-law-mul-add-Algebra-Left-Module-Ring :
+    (r : type-Ring R) (x y : type-Algebra-Left-Module-Ring) →
+    mul-Algebra-Left-Module-Ring r
+      ( add-Algebra-Left-Module-Ring x y) ＝
+    add-Algebra-Left-Module-Ring
+      ( mul-Algebra-Left-Module-Ring r x)
+      ( mul-Algebra-Left-Module-Ring r y)
+  left-distributive-law-mul-add-Algebra-Left-Module-Ring r x y =
+    satisfies-A
+      ( left-distributive-mul-add-law-left-module-Ring r)
+      ( component-tuple 2 (y ∷ x ∷ empty-tuple))
+
+  right-distributive-law-mul-add-Algebra-Left-Module-Ring :
+    (r s : type-Ring R) (x : type-Algebra-Left-Module-Ring) →
+    mul-Algebra-Left-Module-Ring (add-Ring R r s) x ＝
+    add-Algebra-Left-Module-Ring
+      ( mul-Algebra-Left-Module-Ring r x)
+      ( mul-Algebra-Left-Module-Ring s x)
+  right-distributive-law-mul-add-Algebra-Left-Module-Ring r s x =
+    satisfies-A
+      ( right-distributive-mul-add-law-left-module-Ring r s)
+      ( λ _ → x)
+
+  associative-mul-Algebra-Left-Module-Ring :
+    (r s : type-Ring R) (x : type-Algebra-Left-Module-Ring) →
+    mul-Algebra-Left-Module-Ring (mul-Ring R r s) x ＝
+    mul-Algebra-Left-Module-Ring r (mul-Algebra-Left-Module-Ring s x)
+  associative-mul-Algebra-Left-Module-Ring r s x =
+    satisfies-A
+      ( associative-mul-law-left-module-Ring r s)
+      ( λ _ → x)
+
+  left-unit-law-mul-Algebra-Left-Module-Ring :
+    (x : type-Algebra-Left-Module-Ring) →
+    mul-Algebra-Left-Module-Ring (one-Ring R) x ＝ x
+  left-unit-law-mul-Algebra-Left-Module-Ring x =
+    satisfies-A left-unit-mul-law-left-module-Ring (λ _ → x)
+
+  left-module-Algebra-Left-Module-Ring : left-module-Ring l2 R
+  left-module-Algebra-Left-Module-Ring =
+    make-left-module-Ring
+      ( R)
+      ( ab-Algebra-Left-Module-Ring)
+      ( mul-Algebra-Left-Module-Ring)
+      ( left-distributive-law-mul-add-Algebra-Left-Module-Ring)
+      ( right-distributive-law-mul-add-Algebra-Left-Module-Ring)
+      ( left-unit-law-mul-Algebra-Left-Module-Ring)
+      ( associative-mul-Algebra-Left-Module-Ring)
+```
+
+### Algebras in the theory of left modules over rings from left modules over rings
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  where
+
+  algebra-ab-left-module-Ring : Algebra-Ab l2
+  algebra-ab-left-module-Ring = algebra-ab-Ab (ab-left-module-Ring R M)
+
+  is-model-set-left-module-Ring :
+    is-model-of-signature
+      ( signature-left-module-Ring R)
+      ( set-left-module-Ring R M)
+  is-model-set-left-module-Ring (operation-left-module-ring-operation-Ab op) =
+    is-model-set-Algebra
+      ( signature-Ab)
+      ( algebraic-theory-Ab)
+      ( algebra-ab-left-module-Ring)
+      ( op)
+  is-model-set-left-module-Ring
+    (mul-operation-left-module-Ring r) (x ∷ empty-tuple) =
+    mul-left-module-Ring R M r x
+
+  model-left-module-Ring :
+    Model-Of-Signature l2 (signature-left-module-Ring R)
+  model-left-module-Ring =
+    ( set-left-module-Ring R M ,
+      is-model-set-left-module-Ring)
+
+  is-algebra-model-left-module-Ring :
+    is-algebra-Model-of-Signature
+      ( signature-left-module-Ring R)
+      ( algebraic-theory-left-module-Ring R)
+      ( model-left-module-Ring)
+  is-algebra-model-left-module-Ring associative-add-law-left-module-Ring xs =
+    associative-add-left-module-Ring R M _ _ _
+  is-algebra-model-left-module-Ring left-unit-add-law-left-module-Ring xs =
+    left-unit-law-add-left-module-Ring R M _
+  is-algebra-model-left-module-Ring right-unit-add-law-left-module-Ring xs =
+    right-unit-law-add-left-module-Ring R M _
+  is-algebra-model-left-module-Ring left-inverse-add-law-left-module-Ring xs =
+    left-inverse-law-add-left-module-Ring R M _
+  is-algebra-model-left-module-Ring right-inverse-add-law-left-module-Ring xs =
+    right-inverse-law-add-left-module-Ring R M _
+  is-algebra-model-left-module-Ring
+    (left-distributive-mul-add-law-left-module-Ring r) xs =
+    left-distributive-mul-add-left-module-Ring R M r _ _
+  is-algebra-model-left-module-Ring
+    (right-distributive-mul-add-law-left-module-Ring r s) xs =
+    right-distributive-mul-add-left-module-Ring R M r s _
+  is-algebra-model-left-module-Ring commutative-add-law-left-module-Ring xs =
+    commutative-add-left-module-Ring R M _ _
+  is-algebra-model-left-module-Ring left-unit-mul-law-left-module-Ring xs =
+    left-unit-law-mul-left-module-Ring R M _
+  is-algebra-model-left-module-Ring
+    (associative-mul-law-left-module-Ring r s) xs =
+    associative-mul-left-module-Ring R M r s _
+
+  algebra-left-module-left-module-Ring :
+    Algebra-Left-Module-Ring l2 R
+  algebra-left-module-left-module-Ring =
+    ( model-left-module-Ring , is-algebra-model-left-module-Ring)
+```
+
+### The type of left modules over rings is equivalent to the type of algebras in the theory of left modules
+
+```agda
+module _
+  {l1 l2 : Level}
+  (R : Ring l1)
+  where
+
+  abstract
+    is-section-left-module-Algebra-Left-Module-Ring :
+      (A : Algebra-Left-Module-Ring l2 R) →
+      algebra-left-module-left-module-Ring R
+        ( left-module-Algebra-Left-Module-Ring R A) ＝
+      A
+    is-section-left-module-Algebra-Left-Module-Ring A =
+      eq-type-subtype
+        ( is-algebra-prop-Model-Of-Signature
+          ( signature-left-module-Ring R)
+          ( algebraic-theory-left-module-Ring R))
+        ( eq-pair-eq-fiber
+          ( eq-binary-htpy _ _
+            λ where
+              add-operation-left-module-Ring (x ∷ y ∷ empty-tuple) → refl
+              neg-operation-left-module-Ring (x ∷ empty-tuple) → refl
+              zero-operation-left-module-Ring empty-tuple → refl
+              (mul-operation-left-module-Ring r) (x ∷ empty-tuple) → refl))
+
+    is-retraction-left-module-Algebra-Left-Module-Ring :
+      (M : left-module-Ring l2 R) →
+      left-module-Algebra-Left-Module-Ring R
+        ( algebra-left-module-left-module-Ring R M) ＝
+      M
+    is-retraction-left-module-Algebra-Left-Module-Ring M =
+      let
+        A = ab-left-module-Ring R M
+      in
+        eq-pair-eq-fiber
+          ( eq-htpy-hom-Ring
+            ( R)
+            ( endomorphism-ring-Ab A)
+            ( _)
+            ( _)
+            ( λ r → eq-htpy-hom-Ab A A refl-htpy))
+
+  is-equiv-algebra-left-module-left-module-Ring :
+    is-equiv
+      ( algebra-left-module-left-module-Ring {l2 = l2} R)
+  is-equiv-algebra-left-module-left-module-Ring =
+    is-equiv-is-invertible
+      ( left-module-Algebra-Left-Module-Ring R)
+      ( is-section-left-module-Algebra-Left-Module-Ring)
+      ( is-retraction-left-module-Algebra-Left-Module-Ring)
+
+  equiv-left-module-Algebra-Left-Module-Ring :
+    left-module-Ring l2 R ≃ Algebra-Left-Module-Ring l2 R
+  equiv-left-module-Algebra-Left-Module-Ring =
+    ( algebra-left-module-left-module-Ring R ,
+      is-equiv-algebra-left-module-left-module-Ring)
+```
+
+### Linear maps on left modules are equivalent to homomorphisms of algebras in the theory of left modules
+
+```agda
+hom-Algebra-Left-Module-Ring :
+  {l1 l2 l3 : Level} (R : Ring l1) →
+  Algebra-Left-Module-Ring l2 R → Algebra-Left-Module-Ring l3 R →
+  UU (l1 ⊔ l2 ⊔ l3)
+hom-Algebra-Left-Module-Ring R =
+  hom-Algebra
+    ( signature-left-module-Ring R)
+    ( algebraic-theory-left-module-Ring R)
+
+linear-map-left-module-hom-Algebra-Left-Module-Ring :
+  {l1 l2 l3 : Level} (R : Ring l1)
+  (A : Algebra-Left-Module-Ring l2 R)
+  (B : Algebra-Left-Module-Ring l3 R) →
+  hom-Algebra-Left-Module-Ring R A B →
+  linear-map-left-module-Ring R
+    ( left-module-Algebra-Left-Module-Ring R A)
+    ( left-module-Algebra-Left-Module-Ring R B)
+linear-map-left-module-hom-Algebra-Left-Module-Ring
+  R A B (φ , preserves-ops-φ) =
+  ( φ ,
+    ( λ x y →
+      preserves-ops-φ add-operation-left-module-Ring (x ∷ y ∷ empty-tuple)) ,
+    ( λ r x →
+      preserves-ops-φ (mul-operation-left-module-Ring r) (x ∷ empty-tuple)))
+
+module _
+  {l1 l2 l3 : Level}
+  (R : Ring l1)
+  (M : left-module-Ring l2 R)
+  (N : left-module-Ring l3 R)
+  where
+
+  hom-algebra-left-module-linear-map-left-module-Ring :
+    linear-map-left-module-Ring R M N →
+    hom-Algebra-Left-Module-Ring R
+      ( algebra-left-module-left-module-Ring R M)
+      ( algebra-left-module-left-module-Ring R N)
+  hom-algebra-left-module-linear-map-left-module-Ring φ =
+    ( map-linear-map-left-module-Ring R M N φ ,
+      λ where
+        zero-operation-left-module-Ring empty-tuple →
+          is-zero-map-zero-linear-map-left-module-Ring R M N φ
+        add-operation-left-module-Ring (x ∷ y ∷ empty-tuple) →
+          is-additive-map-linear-map-left-module-Ring R M N φ x y
+        neg-operation-left-module-Ring (x ∷ empty-tuple) →
+          map-neg-linear-map-left-module-Ring R M N φ x
+        (mul-operation-left-module-Ring r) (x ∷ empty-tuple) →
+          is-homogeneous-map-linear-map-left-module-Ring R M N φ r x)
+
+  is-equiv-hom-algebra-left-module-linear-map-left-module-Ring :
+    is-equiv hom-algebra-left-module-linear-map-left-module-Ring
+  is-equiv-hom-algebra-left-module-linear-map-left-module-Ring =
+    is-equiv-is-invertible
+      ( λ φ@(map-φ , preserves-ops-φ) →
+        -- redoing this definition is easier than doing transport along
+        -- is-retraction-left-module-Algebra-Left-Module-Ring
+        ( map-φ ,
+          ( λ x y →
+            preserves-ops-φ
+              ( add-operation-left-module-Ring)
+              ( x ∷ y ∷ empty-tuple)) ,
+        ( λ r x →
+          preserves-ops-φ
+            ( mul-operation-left-module-Ring r)
+            ( x ∷ empty-tuple))))
+      ( λ φ →
+        eq-htpy-hom-Algebra
+          ( signature-left-module-Ring R)
+          ( algebraic-theory-left-module-Ring R)
+          ( _)
+          ( _)
+          ( _)
+          ( _)
+          ( refl-htpy))
+      ( λ φ → eq-htpy-linear-map-left-module-Ring R M N _ _ refl-htpy)
+
+  equiv-linear-map-hom-algebra-Left-Module-Ring :
+    linear-map-left-module-Ring R M N ≃
+    hom-Algebra-Left-Module-Ring R
+      ( algebra-left-module-left-module-Ring R M)
+      ( algebra-left-module-left-module-Ring R N)
+  equiv-linear-map-hom-algebra-Left-Module-Ring =
+    ( hom-algebra-left-module-linear-map-left-module-Ring ,
+      is-equiv-hom-algebra-left-module-linear-map-left-module-Ring)
+```
diff --git a/src/universal-algebra/algebraic-theory-of-monoids.lagda.md b/src/universal-algebra/algebraic-theory-of-monoids.lagda.md
new file mode 100644
index 0000000000..8039a388d9
--- /dev/null
+++ b/src/universal-algebra/algebraic-theory-of-monoids.lagda.md
@@ -0,0 +1,303 @@
+# The algebraic theory of monoids
+
+```agda
+module universal-algebra.algebraic-theory-of-monoids where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-homotopies
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.injective-maps
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.unital-binary-operations
+open import foundation.universe-levels
+
+open import group-theory.homomorphisms-monoids
+open import group-theory.monoids
+open import group-theory.semigroups
+
+open import lists.tuples
+
+open import univalent-combinatorics.standard-finite-types
+
+open import universal-algebra.abstract-equations-over-signatures
+open import universal-algebra.algebraic-theories
+open import universal-algebra.algebraic-theory-of-semigroups
+open import universal-algebra.algebras
+open import universal-algebra.extensions-signatures
+open import universal-algebra.homomorphisms-of-algebras
+open import universal-algebra.models-of-signatures
+open import universal-algebra.signatures
+open import universal-algebra.terms-over-signatures
+```
+
+</details>
+
+## Idea
+
+There is an
+{{#concept "algebraic theory of monoids" Agda=algebraic-theory-Monoid}}. The
+type of all such [algebras](universal-algebra.algebras.md) is
+[equivalent](foundation-core.equivalences.md) to the type of
+[monoids](group-theory.monoids.md).
+
+## Definition
+
+```agda
+data operation-Monoid : UU lzero where
+  operation-monoid-operation-Semigroup : operation-Semigroup → operation-Monoid
+  unit-operation-Monoid : operation-Monoid
+
+pattern mul-operation-Monoid =
+  operation-monoid-operation-Semigroup mul-operation-Semigroup
+
+signature-Monoid : signature lzero
+pr1 signature-Monoid = operation-Monoid
+pr2 signature-Monoid (operation-monoid-operation-Semigroup op) =
+  arity-operation-signature signature-Semigroup op
+pr2 signature-Monoid unit-operation-Monoid = 0
+
+data law-Monoid : UU lzero where
+  law-monoid-law-Semigroup : law-Semigroup → law-Monoid
+  left-unit-mul-law-Monoid : law-Monoid
+  right-unit-mul-law-Monoid : law-Monoid
+
+pattern associative-mul-law-Monoid =
+  law-monoid-law-Semigroup associative-mul-law-Semigroup
+
+extension-signature-semigroup-Monoid :
+  is-extension-of-signature signature-Semigroup signature-Monoid
+pr1 extension-signature-semigroup-Monoid =
+  operation-monoid-operation-Semigroup
+pr2 extension-signature-semigroup-Monoid _ = refl
+
+algebraic-theory-Monoid : Algebraic-Theory lzero signature-Monoid
+pr1 algebraic-theory-Monoid = law-Monoid
+pr2 algebraic-theory-Monoid =
+  let
+    x-term = var-term (zero-Fin 0)
+    _*-term_ x y = op-term mul-operation-Monoid (x ∷ y ∷ empty-tuple)
+    unit-term = op-term unit-operation-Monoid empty-tuple
+  in
+    λ where
+      (law-monoid-law-Semigroup law) →
+        translation-abstract-equation
+          ( signature-Semigroup)
+          ( signature-Monoid)
+          ( extension-signature-semigroup-Monoid)
+          ( index-abstract-equation-Algebraic-Theory
+            ( signature-Semigroup)
+            ( algebraic-theory-Semigroup)
+            ( law))
+      left-unit-mul-law-Monoid →
+        ( 1 ,
+          unit-term *-term x-term ,
+          x-term)
+      right-unit-mul-law-Monoid →
+        ( 1 ,
+          x-term *-term unit-term ,
+          x-term)
+
+Algebra-Monoid : (l : Level) → UU (lsuc l)
+Algebra-Monoid l =
+  Algebra l signature-Monoid algebraic-theory-Monoid
+```
+
+## Properties
+
+### Algebras in the theory of monoids from monoids
+
+```agda
+module _
+  {l : Level}
+  (M : Monoid l)
+  where
+
+  algebra-semigroup-Monoid : Algebra-Semigroup l
+  algebra-semigroup-Monoid =
+    algebra-semigroup-Semigroup (semigroup-Monoid M)
+
+  is-model-set-Monoid : is-model-of-signature signature-Monoid (set-Monoid M)
+  is-model-set-Monoid (operation-monoid-operation-Semigroup op) =
+    is-model-set-Algebra
+      ( signature-Semigroup)
+      ( algebraic-theory-Semigroup)
+      ( algebra-semigroup-Monoid)
+      ( op)
+  is-model-set-Monoid unit-operation-Monoid empty-tuple = unit-Monoid M
+
+  model-set-Monoid : Model-Of-Signature l signature-Monoid
+  model-set-Monoid =
+    ( set-Monoid M ,
+      is-model-set-Monoid)
+
+  is-algebra-model-set-Monoid :
+    is-algebra-Model-of-Signature
+      ( signature-Monoid)
+      ( algebraic-theory-Monoid)
+      ( model-set-Monoid)
+  is-algebra-model-set-Monoid associative-mul-law-Monoid _ =
+    associative-mul-Monoid M _ _ _
+  is-algebra-model-set-Monoid left-unit-mul-law-Monoid _ =
+    left-unit-law-mul-Monoid M _
+  is-algebra-model-set-Monoid right-unit-mul-law-Monoid _ =
+    right-unit-law-mul-Monoid M _
+
+  algebra-monoid-Monoid : Algebra-Monoid l
+  algebra-monoid-Monoid =
+    ( model-set-Monoid ,
+      is-algebra-model-set-Monoid)
+```
+
+### Monoids from algebras in the theory of monoids
+
+```agda
+module _
+  {l : Level}
+  (A@((set-A , model-A) , satisfies-A) : Algebra-Monoid l)
+  where
+
+  algebra-semigroup-Algebra-Monoid : Algebra-Semigroup l
+  algebra-semigroup-Algebra-Monoid =
+    ( ( set-A ,
+        model-A ∘ operation-monoid-operation-Semigroup) ,
+      λ where
+        associative-mul-law-Semigroup → satisfies-A associative-mul-law-Monoid)
+
+  semigroup-Algebra-Monoid : Semigroup l
+  semigroup-Algebra-Monoid =
+    semigroup-Algebra-Semigroup algebra-semigroup-Algebra-Monoid
+
+  type-Algebra-Monoid : UU l
+  type-Algebra-Monoid = type-Set set-A
+
+  mul-Algebra-Monoid :
+    type-Algebra-Monoid → type-Algebra-Monoid → type-Algebra-Monoid
+  mul-Algebra-Monoid = mul-Semigroup semigroup-Algebra-Monoid
+
+  unit-Algebra-Monoid : type-Algebra-Monoid
+  unit-Algebra-Monoid = model-A unit-operation-Monoid empty-tuple
+
+  left-unit-law-mul-Algebra-Monoid :
+    left-unit-law mul-Algebra-Monoid unit-Algebra-Monoid
+  left-unit-law-mul-Algebra-Monoid x =
+    satisfies-A left-unit-mul-law-Monoid (λ _ → x)
+
+  right-unit-law-mul-Algebra-Monoid :
+    right-unit-law mul-Algebra-Monoid unit-Algebra-Monoid
+  right-unit-law-mul-Algebra-Monoid x =
+    satisfies-A right-unit-mul-law-Monoid (λ _ → x)
+
+  monoid-Algebra-Monoid : Monoid l
+  monoid-Algebra-Monoid =
+    ( semigroup-Algebra-Monoid ,
+      unit-Algebra-Monoid ,
+      left-unit-law-mul-Algebra-Monoid ,
+      right-unit-law-mul-Algebra-Monoid)
+```
+
+### The type of monoids is equivalent to the type of algebras in the theory of monoids
+
+```agda
+abstract
+  is-section-monoid-Algebra-Monoid :
+    {l : Level} (A : Algebra-Monoid l) →
+    algebra-monoid-Monoid (monoid-Algebra-Monoid A) ＝ A
+  is-section-monoid-Algebra-Monoid ((set-A , model-A) , satisfies-A) =
+    eq-type-subtype
+      ( is-algebra-prop-Model-Of-Signature
+        ( signature-Monoid)
+        ( algebraic-theory-Monoid))
+      ( eq-pair-eq-fiber
+        ( eq-binary-htpy _ _
+          ( λ where
+            mul-operation-Monoid (x ∷ y ∷ empty-tuple) → refl
+            unit-operation-Monoid empty-tuple → refl)))
+
+  is-retraction-monoid-Algebra-Monoid :
+    {l : Level} (M : Monoid l) →
+    monoid-Algebra-Monoid (algebra-monoid-Monoid M) ＝ M
+  is-retraction-monoid-Algebra-Monoid _ = refl
+
+is-equiv-algebra-monoid-Monoid :
+  {l : Level} → is-equiv (algebra-monoid-Monoid {l})
+is-equiv-algebra-monoid-Monoid =
+  is-equiv-is-invertible
+    ( monoid-Algebra-Monoid)
+    ( is-section-monoid-Algebra-Monoid)
+    ( is-retraction-monoid-Algebra-Monoid)
+
+equiv-algebra-monoid-Monoid :
+  {l : Level} → Monoid l ≃ Algebra-Monoid l
+equiv-algebra-monoid-Monoid =
+  ( algebra-monoid-Monoid ,
+    is-equiv-algebra-monoid-Monoid)
+```
+
+### Homomorphisms of monoids are equivalent to homomorphisms in the algebra of monoids
+
+```agda
+hom-Algebra-Monoid :
+  {l1 l2 : Level} → Algebra-Monoid l1 → Algebra-Monoid l2 → UU (l1 ⊔ l2)
+hom-Algebra-Monoid =
+  hom-Algebra signature-Monoid algebraic-theory-Monoid
+
+hom-monoid-hom-Algebra-Monoid :
+  {l1 l2 : Level} (M : Algebra-Monoid l1) (N : Algebra-Monoid l2) →
+  hom-Algebra-Monoid M N →
+  hom-Monoid (monoid-Algebra-Monoid M) (monoid-Algebra-Monoid N)
+hom-monoid-hom-Algebra-Monoid M N (f , preserves-ops-f) =
+  ( (f , preserves-ops-f mul-operation-Monoid (_ ∷ _ ∷ empty-tuple)) ,
+    preserves-ops-f unit-operation-Monoid empty-tuple)
+
+module _
+  {l1 l2 : Level}
+  (M : Monoid l1)
+  (N : Monoid l2)
+  where
+
+  hom-algebra-monoid-hom-Monoid :
+    hom-Monoid M N →
+    hom-Algebra-Monoid (algebra-monoid-Monoid M) (algebra-monoid-Monoid N)
+  hom-algebra-monoid-hom-Monoid
+    ((f , preserves-mul-f) , preserves-unit-f) =
+    ( f ,
+      λ where
+        mul-operation-Monoid (x ∷ y ∷ empty-tuple) → preserves-mul-f
+        unit-operation-Monoid empty-tuple → preserves-unit-f)
+
+  is-equiv-hom-algebra-monoid-hom-Monoid :
+    is-equiv hom-algebra-monoid-hom-Monoid
+  is-equiv-hom-algebra-monoid-hom-Monoid =
+    is-equiv-is-invertible
+      ( hom-monoid-hom-Algebra-Monoid
+        ( algebra-monoid-Monoid M)
+        ( algebra-monoid-Monoid N))
+      ( λ φ →
+        eq-htpy-hom-Algebra
+          ( signature-Monoid)
+          ( algebraic-theory-Monoid)
+          ( algebra-monoid-Monoid M)
+          ( algebra-monoid-Monoid N)
+          ( _)
+          ( φ)
+          ( refl-htpy))
+      ( λ φ → eq-htpy-hom-Monoid M N _ φ refl-htpy)
+
+  equiv-hom-algebra-hom-Algebra-Monoid :
+    hom-Monoid M N ≃
+    hom-Algebra-Monoid (algebra-monoid-Monoid M) (algebra-monoid-Monoid N)
+  equiv-hom-algebra-hom-Algebra-Monoid =
+    ( hom-algebra-monoid-hom-Monoid ,
+      is-equiv-hom-algebra-monoid-hom-Monoid)
+```
diff --git a/src/universal-algebra/algebraic-theory-of-semigroups.lagda.md b/src/universal-algebra/algebraic-theory-of-semigroups.lagda.md
new file mode 100644
index 0000000000..c5fb2ac249
--- /dev/null
+++ b/src/universal-algebra/algebraic-theory-of-semigroups.lagda.md
@@ -0,0 +1,231 @@
+# The algebraic theory of semigroups
+
+```agda
+module universal-algebra.algebraic-theory-of-semigroups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.modular-arithmetic-standard-finite-types
+open import elementary-number-theory.natural-numbers
+
+open import foundation.binary-homotopies
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.equivalences
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import group-theory.homomorphisms-semigroups
+open import group-theory.semigroups
+
+open import lists.tuples
+
+open import universal-algebra.algebraic-theories
+open import universal-algebra.algebras
+open import universal-algebra.homomorphisms-of-algebras
+open import universal-algebra.models-of-signatures
+open import universal-algebra.signatures
+open import universal-algebra.terms-over-signatures
+```
+
+</details>
+
+## Idea
+
+There is an
+{{#concept "algebraic theory of semigroups" Agda=algebraic-theory-Semigroup}}.
+The type of all such [algebras](universal-algebra.algebras.md) is
+[equivalent](foundation-core.equivalences.md) to the type of
+[semigroups](group-theory.semigroups.md).
+
+## Definition
+
+```agda
+data operation-Semigroup : UU lzero where
+  mul-operation-Semigroup : operation-Semigroup
+
+signature-Semigroup : signature lzero
+pr1 signature-Semigroup = operation-Semigroup
+pr2 signature-Semigroup mul-operation-Semigroup = 2
+
+data law-Semigroup : UU lzero where
+  associative-mul-law-Semigroup : law-Semigroup
+
+algebraic-theory-Semigroup : Algebraic-Theory lzero signature-Semigroup
+pr1 algebraic-theory-Semigroup = law-Semigroup
+pr2 algebraic-theory-Semigroup associative-mul-law-Semigroup =
+  let
+    var : (i : ℕ) → term signature-Semigroup 3
+    var i = var-term (mod-succ-ℕ 2 i)
+    _*_ x y = op-term mul-operation-Semigroup (x ∷ y ∷ empty-tuple)
+  in
+    ( 3 ,
+      (var 0 * var 1) * var 2 ,
+      var 0 * (var 1 * var 2))
+
+Algebra-Semigroup : (l : Level) → UU (lsuc l)
+Algebra-Semigroup l =
+  Algebra l signature-Semigroup algebraic-theory-Semigroup
+```
+
+## Properties
+
+### The algebra of semigroups is equivalent to the type of semigroups
+
+```agda
+module _
+  {l : Level}
+  (((set-A , models-A) , satisfies-A) : Algebra-Semigroup l)
+  where
+
+  type-Algebra-Semigroup : UU l
+  type-Algebra-Semigroup = type-Set set-A
+
+  mul-Algebra-Semigroup :
+    type-Algebra-Semigroup → type-Algebra-Semigroup → type-Algebra-Semigroup
+  mul-Algebra-Semigroup x y =
+    models-A mul-operation-Semigroup (x ∷ y ∷ empty-tuple)
+
+  associative-mul-Algebra-Semigroup :
+    (x y z : type-Algebra-Semigroup) →
+    mul-Algebra-Semigroup (mul-Algebra-Semigroup x y) z ＝
+    mul-Algebra-Semigroup x (mul-Algebra-Semigroup y z)
+  associative-mul-Algebra-Semigroup x y z =
+    satisfies-A
+      ( associative-mul-law-Semigroup)
+      ( component-tuple 3 (z ∷ y ∷ x ∷ empty-tuple))
+
+  semigroup-Algebra-Semigroup : Semigroup l
+  semigroup-Algebra-Semigroup =
+    ( set-A ,
+      mul-Algebra-Semigroup ,
+      associative-mul-Algebra-Semigroup)
+
+module _
+  {l : Level}
+  (G : Semigroup l)
+  where
+
+  is-model-Semigroup :
+    is-model-of-signature signature-Semigroup (set-Semigroup G)
+  is-model-Semigroup
+    mul-operation-Semigroup (x ∷ y ∷ empty-tuple) =
+    mul-Semigroup G x y
+
+  model-Semigroup :
+    Model-Of-Signature l signature-Semigroup
+  model-Semigroup = (set-Semigroup G , is-model-Semigroup)
+
+  is-algebra-model-Semigroup :
+    is-algebra-Model-of-Signature
+      ( signature-Semigroup)
+      ( algebraic-theory-Semigroup)
+      ( model-Semigroup)
+  is-algebra-model-Semigroup associative-mul-law-Semigroup xs =
+    associative-mul-Semigroup G _ _ _
+
+  algebra-semigroup-Semigroup : Algebra-Semigroup l
+  algebra-semigroup-Semigroup =
+    ( model-Semigroup ,
+      is-algebra-model-Semigroup)
+
+abstract
+  is-section-semigroup-Algebra-Semigroup :
+    {l : Level} (A : Algebra-Semigroup l) →
+    algebra-semigroup-Semigroup (semigroup-Algebra-Semigroup A) ＝ A
+  is-section-semigroup-Algebra-Semigroup A =
+    eq-type-subtype
+      ( is-algebra-prop-Model-Of-Signature
+        ( signature-Semigroup)
+        ( algebraic-theory-Semigroup))
+      ( eq-pair-eq-fiber
+        ( eq-binary-htpy _ _
+          λ where
+            mul-operation-Semigroup (x ∷ y ∷ empty-tuple) → refl))
+
+  is-retraction-semigroup-Algebra-Semigroup :
+    {l : Level} (G : Semigroup l) →
+    semigroup-Algebra-Semigroup (algebra-semigroup-Semigroup G) ＝ G
+  is-retraction-semigroup-Algebra-Semigroup G = refl
+
+is-equiv-semigroup-Algebra-Semigroup :
+  {l : Level} → is-equiv (algebra-semigroup-Semigroup {l})
+is-equiv-semigroup-Algebra-Semigroup =
+  is-equiv-is-invertible
+    ( semigroup-Algebra-Semigroup)
+    ( is-section-semigroup-Algebra-Semigroup)
+    ( is-retraction-semigroup-Algebra-Semigroup)
+
+equiv-semigroup-Algebra-Semigroup :
+  {l : Level} → Semigroup l ≃ Algebra-Semigroup l
+equiv-semigroup-Algebra-Semigroup =
+  ( algebra-semigroup-Semigroup ,
+    is-equiv-semigroup-Algebra-Semigroup)
+```
+
+### Homomorphisms of semigroups are equivalent to homomorphisms of the algebras of semigroups
+
+```agda
+hom-Algebra-Semigroup :
+  {l1 l2 : Level} → Algebra-Semigroup l1 → Algebra-Semigroup l2 → UU (l1 ⊔ l2)
+hom-Algebra-Semigroup =
+  hom-Algebra signature-Semigroup algebraic-theory-Semigroup
+
+hom-semigroup-hom-Algebra-Semigroup :
+  {l1 l2 : Level} (G : Algebra-Semigroup l1) (H : Algebra-Semigroup l2) →
+  hom-Algebra-Semigroup G H →
+  hom-Semigroup
+    ( semigroup-Algebra-Semigroup G)
+    ( semigroup-Algebra-Semigroup H)
+hom-semigroup-hom-Algebra-Semigroup G H (map-f , preserves-ops-f) =
+  ( map-f ,
+    preserves-ops-f mul-operation-Semigroup (_ ∷ _ ∷ empty-tuple))
+
+module _
+  {l1 l2 : Level}
+  (G : Semigroup l1)
+  (H : Semigroup l2)
+  where
+
+  hom-algebra-semigroup-hom-Semigroup :
+    hom-Semigroup G H →
+    hom-Algebra-Semigroup
+      ( algebra-semigroup-Semigroup G)
+      ( algebra-semigroup-Semigroup H)
+  hom-algebra-semigroup-hom-Semigroup (map-f , preserves-mul-f) =
+    ( map-f ,
+      λ where
+        mul-operation-Semigroup (x ∷ y ∷ empty-tuple) → preserves-mul-f)
+
+  is-equiv-hom-algebra-semigroup-hom-Semigroup :
+    is-equiv hom-algebra-semigroup-hom-Semigroup
+  is-equiv-hom-algebra-semigroup-hom-Semigroup =
+    is-equiv-is-invertible
+      ( hom-semigroup-hom-Algebra-Semigroup
+        ( algebra-semigroup-Semigroup G)
+        ( algebra-semigroup-Semigroup H))
+      ( λ φ →
+        eq-htpy-hom-Algebra
+          ( signature-Semigroup)
+          ( algebraic-theory-Semigroup)
+          ( algebra-semigroup-Semigroup G)
+          ( algebra-semigroup-Semigroup H)
+          ( _)
+          ( φ)
+          ( refl-htpy))
+      ( λ φ → eq-htpy-hom-Semigroup G H refl-htpy)
+
+  equiv-hom-semigroup-hom-Algebra-Semigroup :
+    hom-Semigroup G H ≃
+    hom-Algebra-Semigroup
+      ( algebra-semigroup-Semigroup G)
+      ( algebra-semigroup-Semigroup H)
+  equiv-hom-semigroup-hom-Algebra-Semigroup =
+    ( hom-algebra-semigroup-hom-Semigroup ,
+      is-equiv-hom-algebra-semigroup-hom-Semigroup)
+```
diff --git a/src/universal-algebra/algebras.lagda.md b/src/universal-algebra/algebras.lagda.md
index df1c56cda9..b5c8eeaee7 100644
--- a/src/universal-algebra/algebras.lagda.md
+++ b/src/universal-algebra/algebras.lagda.md
@@ -13,11 +13,14 @@ open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
 open import foundation.subtype-identity-principle
+open import foundation.subtypes
 open import foundation.torsorial-type-families
 open import foundation.universe-levels
 
 open import foundation-core.equivalences
 
+open import lists.finite-sequences
+
 open import universal-algebra.abstract-equations-over-signatures
 open import universal-algebra.algebraic-theories
 open import universal-algebra.equivalences-models-of-signatures
@@ -47,16 +50,34 @@ module _
   {l1 l2 : Level} (σ : signature l1) (T : Algebraic-Theory l2 σ)
   where
 
-  is-algebra : {l3 : Level} → Model-Of-Signature l3 σ → UU (l2 ⊔ l3)
-  is-algebra M =
-    (e : index-Algebraic-Theory σ T) →
-    (assign : assignment σ (type-Model-Of-Signature σ M)) →
-    eval-term σ (is-model-set-Model-Of-Signature σ M) assign
-      ( lhs-abstract-equation σ
-        ( index-abstract-equation-Algebraic-Theory σ T e)) ＝
-    eval-term σ (is-model-set-Model-Of-Signature σ M) assign
-      ( rhs-abstract-equation σ
-        ( index-abstract-equation-Algebraic-Theory σ T e))
+  is-algebra-prop-Model-Of-Signature :
+    {l3 : Level} → Model-Of-Signature l3 σ → Prop (l2 ⊔ l3)
+  is-algebra-prop-Model-Of-Signature M =
+    Π-Prop
+      ( index-Algebraic-Theory σ T)
+      ( λ e →
+        let
+          (k , lhs , rhs) = index-abstract-equation-Algebraic-Theory σ T e
+          m = is-model-set-Model-Of-Signature σ M
+        in
+          Π-Prop
+            ( fin-sequence (type-Model-Of-Signature σ M) k)
+            ( λ assign →
+              Id-Prop
+                ( set-Model-Of-Signature σ M)
+                ( eval-term σ m assign lhs)
+                ( eval-term σ m assign rhs)))
+
+  is-algebra-Model-of-Signature :
+    {l3 : Level} → Model-Of-Signature l3 σ → UU (l2 ⊔ l3)
+  is-algebra-Model-of-Signature =
+    is-in-subtype is-algebra-prop-Model-Of-Signature
+
+  is-prop-is-algebra-Model-of-Signature :
+    {l3 : Level} (M : Model-Of-Signature l3 σ) →
+    is-prop (is-algebra-Model-of-Signature M)
+  is-prop-is-algebra-Model-of-Signature =
+    is-prop-is-in-subtype is-algebra-prop-Model-Of-Signature
 ```
 
 ### The type of algebras
@@ -68,7 +89,7 @@ Algebra :
   Algebraic-Theory l2 σ →
   UU (l1 ⊔ l2 ⊔ lsuc l3)
 Algebra l3 σ T =
-  Σ (Model-Of-Signature l3 σ) (is-algebra σ T)
+  type-subtype (is-algebra-prop-Model-Of-Signature σ T {l3})
 
 module _
   {l1 l2 l3 : Level} (σ : signature l1)
@@ -90,28 +111,6 @@ module _
   is-set-type-Algebra : is-set type-Algebra
   is-set-type-Algebra = is-set-type-Set set-Algebra
 
-  is-algebra-Algebra : is-algebra σ T model-Algebra
-  is-algebra-Algebra = pr2 A
-```
-
-## Properties
-
-### Being an algebra is a proposition
-
-```agda
-module _
-  {l1 l2 l3 : Level} (σ : signature l1)
-  (T : Algebraic-Theory l2 σ) (X : Model-Of-Signature l3 σ)
-  where
-
-  abstract
-    is-prop-is-algebra : is-prop (is-algebra σ T X)
-    is-prop-is-algebra =
-      is-prop-Π
-        ( λ e →
-          ( is-prop-Π
-            ( λ _ → is-set-type-Model-Of-Signature σ X _ _)))
-
-  is-algebra-Prop : Prop (l2 ⊔ l3)
-  is-algebra-Prop = (is-algebra σ T X , is-prop-is-algebra)
+  is-algebra-model-Algebra : is-algebra-Model-of-Signature σ T model-Algebra
+  is-algebra-model-Algebra = pr2 A
 ```
diff --git a/src/universal-algebra/extensions-signatures.lagda.md b/src/universal-algebra/extensions-signatures.lagda.md
index d7c966c7c6..2641e78be5 100644
--- a/src/universal-algebra/extensions-signatures.lagda.md
+++ b/src/universal-algebra/extensions-signatures.lagda.md
@@ -26,8 +26,7 @@ An
 {{#concept "extension" Disambiguation="of a single-sorted finitary algebraic signature" Agda=is-extension-of-signature}}
 of a
 [single-sorted finitary algebraic signature](universal-algebra.signatures.md)
-`σ` is a signature `τ` such that `σ` [embeds](foundation-core.embeddings.md)
-into `τ` via an arity-preserving map.
+`σ` is a signature `τ` such that `σ` maps into `τ` via an arity-preserving map.
 
 ## Definitions
 
@@ -38,11 +37,11 @@ is-extension-of-signature :
   {l1 l2 : Level} →
   signature l1 → signature l2 → UU (l1 ⊔ l2)
 is-extension-of-signature σ τ =
-  Σ ( operation-signature σ ↪ operation-signature τ)
+  Σ ( operation-signature σ → operation-signature τ)
     ( λ f →
       ( (op : operation-signature σ) →
         arity-operation-signature σ op ＝
-        arity-operation-signature τ (map-emb f op)))
+        arity-operation-signature τ (f op)))
 
 module _
   {l1 l2 : Level}
@@ -50,19 +49,10 @@ module _
   (E : is-extension-of-signature σ τ)
   where
 
-  emb-inclusion-is-extension-of-signature :
-    operation-signature σ ↪ operation-signature τ
-  emb-inclusion-is-extension-of-signature = pr1 E
-
   inclusion-is-extension-of-signature :
     operation-signature σ → operation-signature τ
   inclusion-is-extension-of-signature =
-    map-emb emb-inclusion-is-extension-of-signature
-
-  is-emb-inclusion-is-extension-of-signature :
-    is-emb inclusion-is-extension-of-signature
-  is-emb-inclusion-is-extension-of-signature =
-    is-emb-map-emb emb-inclusion-is-extension-of-signature
+    pr1 E
 
   preserves-arity-inclusion-is-extension-of-signature :
     (op : operation-signature σ) →
diff --git a/src/universal-algebra/isomorphisms-of-algebras.lagda.md b/src/universal-algebra/isomorphisms-of-algebras.lagda.md
index 502ac15785..589cde3c42 100644
--- a/src/universal-algebra/isomorphisms-of-algebras.lagda.md
+++ b/src/universal-algebra/isomorphisms-of-algebras.lagda.md
@@ -193,7 +193,7 @@ module _
       is-equiv (equiv-eq-Algebra A B)
     is-equiv-equiv-eq-Algebra (A , p) =
       subtype-identity-principle
-        ( is-prop-is-algebra σ T)
+        ( is-prop-is-algebra-Model-of-Signature σ T)
         ( p)
         ( id-equiv-Model-Of-Signature σ A)
         ( equiv-eq-Algebra (A , p))
@@ -315,7 +315,7 @@ module _
         ( is-torsorial-equiv-Algebra σ T A)
 
   iso-eq-Algebra :
-      (A B : Algebra l3 σ T) → A ＝ B → iso-Algebra σ T A B
+    (A B : Algebra l3 σ T) → A ＝ B → iso-Algebra σ T A B
   iso-eq-Algebra = iso-eq-Large-Precategory (Algebra-Large-Precategory σ T)
 
   abstract
diff --git a/src/universal-algebra/terms-over-signatures.lagda.md b/src/universal-algebra/terms-over-signatures.lagda.md
index 6886fc9b5a..dc3abdc341 100644
--- a/src/universal-algebra/terms-over-signatures.lagda.md
+++ b/src/universal-algebra/terms-over-signatures.lagda.md
@@ -11,18 +11,18 @@ open import elementary-number-theory.equality-natural-numbers
 open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions
-open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.transport-along-identifications
-open import foundation.unit-type
 open import foundation.universe-levels
 
+open import lists.equivalence-tuples-finite-sequences
+open import lists.finite-sequences
 open import lists.functoriality-tuples
-open import lists.lists
-open import lists.lists-discrete-types
 open import lists.tuples
 
+open import univalent-combinatorics.standard-finite-types
+
 open import universal-algebra.extensions-signatures
 open import universal-algebra.models-of-signatures
 open import universal-algebra.signatures
@@ -50,40 +50,9 @@ module _
   {l1 : Level} (σ : signature l1)
   where
 
-  data term : UU l1 where
-    var-term : ℕ → term
-    op-term : is-model-of-signature-type σ term
-
-  de-bruijn-variables-term : term → list ℕ
-
-  de-bruijn-variables-tuple-term : {n : ℕ} → tuple term n → list ℕ
-
-  de-bruijn-variables-term (var-term x) = cons x nil
-  de-bruijn-variables-term (op-term f x) = de-bruijn-variables-tuple-term x
-
-  de-bruijn-variables-tuple-term empty-tuple = nil
-  de-bruijn-variables-tuple-term (x ∷ v) =
-    union-list
-      has-decidable-equality-ℕ
-        (de-bruijn-variables-term x)
-        (de-bruijn-variables-tuple-term v)
-
-  arity-term : term → ℕ
-  arity-term t = length-list (de-bruijn-variables-term t)
-```
-
-### Assignment of variables
-
-An assignment of variables, assigns each de Bruijn variable to an element in a
-type.
-
-```agda
-module _
-  {l1 : Level} (σ : signature l1)
-  where
-
-  assignment : {l2 : Level} → UU l2 → UU l2
-  assignment A = ℕ → A
+  data term (k : ℕ) : UU l1 where
+    var-term : Fin k → term k
+    op-term : is-model-of-signature-type σ (term k)
 ```
 
 ### Evaluation of terms
@@ -97,81 +66,34 @@ module _
   where
 
   eval-term :
-    {l2 : Level} → {A : UU l2} →
-    is-model-of-signature-type σ A → assignment σ A → term σ → A
+    {l2 : Level} → {A : UU l2} {k : ℕ} →
+    is-model-of-signature-type σ A → fin-sequence A k → term σ k → A
 
   eval-tuple-term :
-    {l2 : Level} → {A : UU l2} {n : ℕ} →
+    {l2 : Level} → {A : UU l2} {m n : ℕ} →
     is-model-of-signature-type σ A →
-    assignment σ A → tuple (term σ) n → tuple A n
+    fin-sequence A m → tuple (term σ m) n → tuple A n
 
   eval-term m assign (var-term n) = assign n
   eval-term m assign (op-term f x) = m f (eval-tuple-term m assign x)
 
+  -- explicit definition required for termination checking;
+  -- we can't use map-tuple
   eval-tuple-term m assign empty-tuple = empty-tuple
   eval-tuple-term m assign (x ∷ v) =
     eval-term m assign x ∷ (eval-tuple-term m assign v)
 
   eval-tuple-map-tuple-eval-term :
-    {l2 : Level} {A : UU l2} {n : ℕ} →
+    {l2 : Level} {A : UU l2} {k n : ℕ} →
     (m : is-model-of-signature-type σ A)
-    (assign : assignment σ A)
-    (v : tuple (term σ) n) →
+    (assign : fin-sequence A k)
+    (v : tuple (term σ k) n) →
     eval-tuple-term m assign v ＝ map-tuple (eval-term m assign) v
   eval-tuple-map-tuple-eval-term m assign empty-tuple = refl
   eval-tuple-map-tuple-eval-term m assign (x ∷ v) =
     ap (eval-term m assign x ∷_) (eval-tuple-map-tuple-eval-term m assign v)
 ```
 
-### Evaluation for constant terms
-
-If a term `t` uses no variables, then any model on a type `A` assigns `t` to an
-element of `A`.
-
-```agda
-module _
-  {l1 : Level} (σ : signature l1)
-  where
-
-  eval-constant-term :
-    {l2 : Level} {A : UU l2} →
-    is-model-of-signature-type σ A →
-    (t : term σ) →
-    (de-bruijn-variables-term σ t ＝ nil) →
-    A
-
-  eval-constant-tuple-term :
-    {l2 : Level} {A : UU l2} {n : ℕ} →
-    (is-model-of-signature-type σ A) →
-    (v : tuple (term σ) n) →
-    (all-tuple (λ t → is-nil-list (de-bruijn-variables-term σ t)) v) →
-    tuple A n
-
-  eval-constant-term m (op-term f x) p =
-    m f (eval-constant-tuple-term m x (all-tuple-lemma x p))
-    where
-    all-tuple-lemma :
-      { n : ℕ}
-      ( v : tuple (term σ) n) →
-      ( de-bruijn-variables-tuple-term σ v ＝ nil) →
-      all-tuple (λ t → is-nil-list (de-bruijn-variables-term σ t)) v
-    all-tuple-lemma empty-tuple p = raise-star
-    all-tuple-lemma (x ∷ v) p =
-      pair
-        ( pr1 (is-nil-lemma p))
-        ( all-tuple-lemma v (pr2 (is-nil-lemma p)))
-      where
-      is-nil-lemma =
-        is-nil-union-is-nil-list
-          ( has-decidable-equality-ℕ)
-          ( de-bruijn-variables-term σ x)
-          ( de-bruijn-variables-tuple-term σ v)
-
-  eval-constant-tuple-term m empty-tuple p = empty-tuple
-  eval-constant-tuple-term m (x ∷ v) (p , p') =
-    eval-constant-term m x p ∷ eval-constant-tuple-term m v p'
-```
-
 ### The induced function by a term on a model
 
 ```agda
@@ -179,44 +101,12 @@ module _
   {l1 : Level} (σ : signature l1)
   where
 
-  tuple-assignment :
-    {l2 : Level} {A : UU l2} →
-    ℕ → (l : list ℕ) →
-    tuple A (succ-ℕ (length-list l)) → assignment σ A
-  tuple-assignment x nil (y ∷ empty-tuple) n = y
-  tuple-assignment x (cons x' l) (y ∷ y' ∷ v) n
-    with
-    ( has-decidable-equality-ℕ x n)
-  ... | inl p = y
-  ... | inr p = tuple-assignment x' l (y' ∷ v) n
-
-  induced-function-term :
-    {l2 : Level} → {A : UU l2} →
-    is-model-of-signature-type σ A → (t : term σ) →
-    tuple A (arity-term σ t) → A
-  induced-function-term {l2} {A} m t v with
-    ( has-decidable-equality-list
-      has-decidable-equality-ℕ
-      (de-bruijn-variables-term σ t) nil)
-  ... | inl p = eval-constant-term σ m t p
-  ... | inr p =
-    eval-term σ m
-      ( tr
-        ( λ n → tuple A n → assignment σ A)
-        ( lenght-tail-is-nonnil-list (de-bruijn-variables-term σ t) p)
-        ( tuple-assignment
-          ( head-is-nonnil-list (de-bruijn-variables-term σ t) p)
-          ( tail-is-nonnil-list (de-bruijn-variables-term σ t) p))
-          ( v))
-      ( t)
-
-  assignment-tuple :
-    {l2 : Level} {A : UU l2} →
-    (l : list ℕ) →
-    assignment σ A →
-    tuple A (length-list l)
-  assignment-tuple nil f = empty-tuple
-  assignment-tuple (cons x l) f = f x ∷ assignment-tuple l f
+  eval-term-tuple :
+    {l2 : Level} {A : UU l2} {k : ℕ} →
+    is-model-of-signature-type σ A → term σ k →
+    tuple A k → A
+  eval-term-tuple m t v =
+    eval-term σ m (fin-sequence-tuple _ v) t
 ```
 
 ### Translation of terms
@@ -227,11 +117,12 @@ module _
   (σ : signature l1)
   (τ : signature l2)
   (E : is-extension-of-signature σ τ)
+  {k : ℕ}
   where
 
-  translation-term : term σ → term τ
+  translation-term : term σ k → term τ k
 
-  translation-tuple-term : {n : ℕ} → tuple (term σ) n → tuple (term τ) n
+  translation-tuple-term : {n : ℕ} → tuple (term σ k) n → tuple (term τ k) n
 
   translation-term (var-term x) =
     var-term x
@@ -239,7 +130,7 @@ module _
     op-term
       ( inclusion-is-extension-of-signature σ τ E f)
       ( tr
-        ( tuple (term τ))
+        ( tuple (term τ k))
         ( preserves-arity-inclusion-is-extension-of-signature σ τ E f)
         ( translation-tuple-term v))