The category of algebras of an algebraic theory

Content created by Fredrik Bakke.

Created on 2025-10-31.
Last modified on 2025-10-31.

module universal-algebra.category-of-algebras-algebraic-theories where
Imports 
open import category-theory.categories
open import category-theory.isomorphisms-in-large-precategories
open import category-theory.large-categories
open import category-theory.large-precategories

open import foundation.dependent-pair-types
open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.universe-levels

open import foundation-core.equality-dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.identity-types

open import universal-algebra.algebraic-theories
open import universal-algebra.algebras
open import universal-algebra.homomorphisms-of-algebras
open import universal-algebra.isomorphisms-of-algebras
open import universal-algebra.models-of-signatures
open import universal-algebra.precategory-of-algebras-algebraic-theories
open import universal-algebra.signatures

Idea

Given an algebraic theory T over a single-sorted finitary algebraic signature σ, we have the large category of T-algebras, which consists of T-algebras and T-algebra homomorphisms.

Definition

The large category of algebras

module _
  {l1 l2 : Level} (σ : signature l1) (T : Algebraic-Theory l2 σ)
  where

  is-large-category-Algebra-Large-Precategory :
    is-large-category-Large-Precategory (Algebra-Large-Precategory σ T)
  is-large-category-Algebra-Large-Precategory = is-equiv-iso-eq-Algebra σ T

  Algebra-Large-Category :
    Large-Category (λ l → l1 ⊔ l2 ⊔ lsuc l) (λ l3 → _⊔_ (l1 ⊔ l3))
  large-precategory-Large-Category Algebra-Large-Category =
    Algebra-Large-Precategory σ T
  is-large-category-Large-Category Algebra-Large-Category =
    is-large-category-Algebra-Large-Precategory

The small category of algebras

module _
  {l1 l2 : Level} (σ : signature l1) (T : Algebraic-Theory l2 σ)
  where

  Algebra-Category : (l3 : Level) → Category (l1 ⊔ l2 ⊔ lsuc l3) (l1 ⊔ l3)
  Algebra-Category =
    category-Large-Category (Algebra-Large-Category σ T)

Recent changes