(Version 2.04 of 02 Feb 2023)
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. github.com/ualib/agda-algebras
Citing this work. See the instructions at agda-algebras/Preface.html.
Primary Contributors. William DeMeo and Jacques Carette
We have organized the library into two main modules, called Base and
Setoid, which are imported below (after the [Preface][] module,
which contains no Agda code). These two modules are mostly independent of one
another. The Base module contains submodules that comprise the first
version of the library. The Setoid contains an alternative version
of the library that is based on setoids. Finally, we have begun work on a third
alternative version of the library, called cubical-agda-algebras, based on
Cubical Agda.
{-# OPTIONS --without-K --exact-split --safe #-}
module agda-algebras where open import Overture -- preliminaries open import Base -- version 1 of the library (based on standard dependent types) open import Setoid -- version 2 of the library (based on setoids) open import Demos -- demonstrations (e.g., proof of the HSP Theorem in a single module) open import Examples
The Demos.HSP module presents a fairly self-contained formal proof of Birkhoff’s HSP Theorem in a single module.
An earlier version of the proof is described in the Birkhoff HSP Theorem Section of the documentation; specifically, see Setoid.Varieties.HSP.
The source code containing the complete formal proof of Birkhoff’s Theorem is available in the agda-algebras GitHub repository; see Demos/HSP.lagda or Setoid/Varieties/HSP.lagda.
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.
Based on the work at
https://gitlab.com/ualib/ualib.gitlab.io.
Updated 02 Feb 2023, 15:01