The Agda Universal Algebra Library, Part 2: Structure

TL;DR

This paper details the Agda Universal Algebra Library's formalization of algebraic structures, focusing on homomorphisms, terms, and subalgebras, demonstrating the use of dependent types for mathematical reasoning.

Contribution

It introduces formalized definitions and proofs of homomorphisms, terms, and subalgebras within the UALib, showcasing advanced use of dependent types in universal algebra.

Findings

Formalized homomorphisms, terms, and subalgebras in Agda

Demonstrated power of dependent types for algebraic reasoning

Provided extensive examples from universal algebra

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 universal algebra, equational logic, and model theory, and as such provides many examples that exhibit the power of inductive and dependent types for representing and reasoning about mathematical structures and equational theories. In this paper, we describe the the types and proofs of the UALib that concern homomorphisms, terms, and subalgebras.