(version 2.03 of 20 Apr 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**. https://gitlab.com/ualib/ualib.gitlab.io.git

**PDF documentation**. ualib-part1.pdf, ualib-part2.pdf (ualib-part3.pdf coming soon)

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

{-# OPTIONS --without-K --exact-split --safe #-} module UALib where open import Preface open import Overture open import Relations open import Algebras open import Homomorphisms open import Terms open import Subalgebras open import Varieties

- Overture
- Relation and Quotient Types
- Algebra Types
- Homomorphism Types
- Types for Terms
- Subalgebra Types
- Equations and Varieties

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

BibTeX citation information.

Based on the work at
https://gitlab.com/ualib/ualib.gitlab.io.

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

*Updated 20 Apr 2021, 23:31*