The Agda Universal Algebra Library

(Version 2.03 of 29 Nov 2021)

Abstract. The Agda Universal Algebra Library is a collection of types and programs (theorems and proofs) that formalizes the foundations of universal algebra in dependent type theory using the Agda proof assistant language.

The library contains definitions of many new types for representing important constructs and theorems comprising a substantial part of the foundations of general (universal) algebra and equational logic. These types are implemented in so called “literate” Agda files (with the .lagda extension), and they are grouped into modules which can be easily imported and integrated into other Agda developments.

To get an idea of the current scope of the library, note that it now includes a formal proof of Birkhoff’s HSP Theorem, which asserts that every variety is an equational class. That is, if 𝒦 is a class of algebras which is closed under the taking of homomorphic images, subalgebras, and arbitrary products, then 𝒦 is the class of all algebras satisfying some set of identities. To our knowledge, ours is the first formal, machine-checked proof of Birkhoff’s Theorem. (If you have evidence refuting this claim, we would love to hear about it; please email us!)

We hope the library is useful to mathematicians and computer scientists who wish to formalize their work in dependent type theory and verify their results with a proof assistant. Indeed, the agda-algebras library aims to become an indispensable companion on our mathematical journeys, helping us authenticate the discoveries we make along the way.

Keywords and phrases. Universal algebra, Equational logic, Martin-Löf Type Theory, Birkhoff’s HSP Theorem, Formalization of mathematics, Agda

Software Repository.

Citing this work. See the instructions at agda-algebras/Preface.html.

Primary Contributors. William DeMeo and Jacques Carette

Brief Contents

The following list of modules imported by the current module, agda-algebras, serves as a brief table of contents.

{-# OPTIONS --without-K --exact-split --safe #-}
module agda-algebras where

open import Preface
open import Overture
open import Relations
open import Equality
open import Adjunction
open import Algebras
open import Homomorphisms
open import Terms
open import Subalgebras
open import Varieties
open import Structures
open import Categories
open import Complexity


Creative Commons License The agda-algebras library and its documentation, by William DeMeo and the agda algebras team, is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.
BibTeX citation information.

stereotypeb Based on the work at

Next Module (Preface) →

Updated 29 Nov 2021, 23:49