Algebraic theories

Content created by Fredrik Bakke, Fernando Chu and Garrett Figueroa.

Created on 2023-03-20.
Last modified on 2025-10-31.

module universal-algebra.algebraic-theories where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import universal-algebra.abstract-equations-over-signatures
open import universal-algebra.signatures

Idea

An algebraic theory is a collection of abstract equations over a single-sorted finitary algebraic signature σ that we consider to ‘hold’ in the theory. It is algebraic in the sense that we only require equations involving function symbols from the signature, in contrast to, say, requiring additional types of relations.

Definitions

Theories

Algebraic-Theory : {l1 : Level} (l2 : Level) → signature l1 → UU (l1 ⊔ lsuc l2)
Algebraic-Theory l2 σ = Σ (UU l2) (λ B → (B → abstract-equation σ))

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

  index-Algebraic-Theory : UU l2
  index-Algebraic-Theory = pr1 T

  index-abstract-equation-Algebraic-Theory :
    index-Algebraic-Theory → abstract-equation σ
  index-abstract-equation-Algebraic-Theory = pr2 T

Recent changes