The Agda Universal Algebra Library, Part 2: Structure

arXiv2103.09092MaRDI QIDQ6362995FDOQ6362995

Publication date: 16 March 2021

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.

Mathematics Subject Classification ID

Equational classes, universal algebra in model theory (03C05) Formalization of mathematics in connection with theorem provers (68V20)

This page was built for publication: The Agda Universal Algebra Library, Part 2: Structure

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6362995)