The Agda Universal Algebra Library and Birkhoff's Theorem in Martin-Löf Dependent Type Theory

Code

• gitlab.com/ualib/ualib.gitlab.io
  In papernone★ 0

Abstract

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.

Reproductions