---

The Agda Universal Algebra Library

---

(version 2.01 of 16 June 2021)

DEPRECATED This is the documentation for the old version of the Agda Universal Algebra Library. For the lastest version, please go to:

https://ualib.github.io/agda-algebras

---

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.¹

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.

---

Brief Contents

{-# 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

---

Detailed Contents

• Preface

• Overture
  • Preliminaries
  • Equality
  • Function Extensionality
  • Inverses
  • Agda’s Universe Hierarchy
• Relation and Quotient Types
  • Discrete Relations
  • Continuous Relations
  • Quotients
  • Truncation
  • Relation Extensionality
• Algebra Types
  • Operations and Signatures
  • Algebras
  • Product Algebras
  • Congruence Relations
• Homomorphism Types
  • Basic Definitions
  • Homomorphism Theorems
  • Isomorphisms
  • Homomorphic Images
• Types for Terms
  • Basic Definitions
  • Term Operations
• Subalgebra Types
  • Subuniverses
  • Subalgebras
  • Univalent Subalgebras
• Equations and Varieties
  • Model Theory and Equational Logic
  • The Inductive Types H, S, P, V
  • Equation Preservation Theorems
  • Free Algebras and Birkhoff’s Theorem

---

License and citations

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.

---

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

Next Module (Preface) →