The Agda Universal Algebra Library

(version 2.03 of 01 Mar 2021)

Author. William DeMeo
Affiliation. Department of Algebra, Charles University in Prague

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

In the latest version of the library we have defined many new types for representing the important constructs and theorems that comprise 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 so that they may be easily imported into other Agda programs.

To give an idea of the current scope of the library, we note that it now includes a complete proof of the Birkhoff HSP Theorem which asserts that every variety is an equational class. That is, if 𝒦 is a class of algebras that is closed under the taking of homomorphic images, subalgebras, and arbitrary products, then 𝒦 is the class of algebras satisfying some set of identities. To our knowledge, ours is the first formal, constructive, machine-checked proof of Birkhoff’s Theorem.1

We hope the library will be useful to mathematicians and computer scientists who wish to formally develop their work in type theory and verify their results with a proof assistant. Indeed, the Agda UALib is (or wants to be when it grows up) an indispensable guide on our mathematical journey, helping us forge new paths to higher peaks, all the time verifying and authenticating what we think we found 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.

PDF documentation. ualib-long.pdf, ualib-short.pdf

Citing this work. To learn how to cite the Agda UALib and its documentation, follow this link.

Brief Contents

{-# OPTIONS --without-K --exact-split --safe #-}

module UALib where

open import Preface
open import Prelude
open import Relations
open import Algebras
open import Homomorphisms
open import Terms
open import Subalgebras
open import Varieties

Detailed Contents

License and citations

Creative Commons License The Agda Universal Algebra Library by William DeMeo is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.
BibTeX citation information.

stereotypeb Based on the work at

1Contact the author if you find any evidence that refutes this claim.

Next Module (Preface) →

Updated 01 Mar 2021, 11:42