The Agda Universal Algebra Library, Part 2: Structure
Logic in Computer Science
2021-03-17 v1 Logic
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.
Keywords
Cite
@article{arxiv.2103.09092,
title = {The Agda Universal Algebra Library, Part 2: Structure},
author = {William DeMeo},
journal= {arXiv preprint arXiv:2103.09092},
year = {2021}
}
Comments
33 pages