Algebraic theories
Content created by Fernando Chu, Fredrik Bakke and Garrett Figueroa.
Created on 2023-03-20.
Last modified on 2025-09-05.
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 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
module _ {l1 : Level} (σ : signature l1) where Theory : (l2 : Level) → UU (l1 ⊔ lsuc l2) Theory l2 = Σ (UU l2) (λ B → (B → Abstract-Equation σ)) index-Theory : {l2 : Level} → Theory l2 → UU l2 index-Theory = pr1 index-Abstract-Equation-Theory : {l2 : Level} (Th : Theory l2) → (index-Theory Th) → Abstract-Equation σ index-Abstract-Equation-Theory Th e = pr2 Th e
Recent changes
- 2025-09-05. Garrett Figueroa. Category of algebras of a theory (#1483).
- 2023-04-28. Fredrik Bakke. Miscellaneous refactoring and small additions (#579).
- 2023-03-20. Fernando Chu. Universal algebra first commit (#522).