A Machine-checked proof of Birkhoff's Variety Theorem in Martin-L\"of Type Theory

TL;DR

This paper presents a formal, machine-checked proof of Birkhoff's Variety Theorem within Martin-L"of dependent type theory using the Agda proof assistant, demonstrating the feasibility of formalizing universal algebra in type theory.

Contribution

It provides a self-contained, constructive proof of Birkhoff's HSP theorem in Agda, showcasing the formalization of universal algebra in dependent type theory.

Findings

Formal proof of Birkhoff's HSP theorem in Agda

Demonstrates the expressiveness of dependent types for algebraic structures

Highlights challenges and solutions in formalizing universal algebra

Abstract

The Agda Universal Algebra Library (agda-algebras) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof assistant. In this paper we draw on and explain many components of the agda-algebras library, which we extract into a single Agda module in order to present a self-contained formal and constructive proof of Birkhoff's HSP theorem in Martin-L\"of dependent type theory. In the course of our presentation, we highlight some of the more challenging aspects of formalizing the basic definitions and theorems of universal algebra in type theory. Nonetheless, we hope this paper and the agda-algebras library serve as further evidence in support of the claim that dependent type theory and the Agda language, despite the technical demands they place on the user, are accessible to working mathematicians (such as ourselves) who possess sufficient patience and resolve to formally verify their results with a proof assistant. Indeed, the agda-algebras library now includes a substantial collection of definitions, theorems, and proofs from universal algebra, illustrating the expressive power of inductive and dependent types for representing and reasoning about general algebraic and relational structures.