Papers › The Agda Universal Algebra Library and Birkhoff's Theorem in Martin-Löf Dependent Type Theory
The Agda Universal Algebra Library and Birkhoff's Theorem in Martin-Löf Dependent Type Theory
William DeMeo
The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in Martin-Löf dependent type theory using the Agda programming language and proof assistant. This paper describes the UALib and demonstrates how it makes Agda more accessible to working mathematicians (like ourselves) as a tool for formally verifying "known" results in general algebra and related fields, as well as for discovering new theorems in these areas. The library already includes a substantial collection of definitions, theorems, and proofs from universal algebra and as such provides many examples that exhibit the power of inductive and dependent types for representing and reasoning about algebraic and relational structures. The first major milestone of the UALib project is a complete proof of Birkhoff's HSP Theorem. To the best of our knowledge, this is the first time Birkhoff's Theorem has been formulated and proved in dependent type theory, and verified with a proof assistant. In this paper we describe the UALib and the formal proof of Birkhoff's theorem, discussing some of the challenges we faced and how these hurdles were overcome. In so doing, we illustrate the effectiveness of dependent type theory, Agda, and the UALib for proving and verifying theorems in universal algebra.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections