The Agda Universal Algebra Library, Part 1: Foundation

TL;DR

This paper introduces the Agda Universal Algebra Library, a formalization of universal algebra foundations in dependent type theory, showcasing definitions, theorems, and proofs that leverage Agda's inductive and dependent types.

Contribution

It presents the initial development of a comprehensive library formalizing universal algebra in Agda, focusing on foundational types and challenging aspects of type theory.

Findings

Includes extensive definitions, theorems, and proofs from algebra and equational logic.

Demonstrates the use of inductive and dependent types for formal reasoning.

Provides insights into the logical foundations and initial modules of the library.

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 dependent type theory using the Agda programming language and proof assistant. The UALib includes a substantial collection of definitions, theorems, and proofs from general algebra and equational logic, including many examples that exhibit the power of inductive and dependent types for representing and reasoning about relations, algebraic structures, and equational theories. In this paper we discuss the logical foundations on which the library is built, and describe the types defined in the first 13 modules of the library. Special attention is given to aspects of the library that seem most interesting or challenging from a type theory or mathematical foundations perspective.