Universal Algebra in UniMath
Gianluca Amato, Matteo Calosci, Marco Maggesi, Cosimo Perini Brogi

TL;DR
This paper introduces a library for Universal Algebra in UniMath, enabling the implementation of term algebras and algebraic structures without inductive types, and demonstrates their categorical and computational properties.
Contribution
It provides a novel, computationally sound implementation of universal algebra concepts in UniMath, including term algebras and categories of algebras, using homotopy W-types and displayed categories.
Findings
Term algebras are instances of homotopy W-types.
Categories of algebras are univalent and initial objects.
Library supports algebraic and propositional logic examples.
Abstract
We present our library for Universal Algebra in the UniMath framework dealing with multi-sorted signatures, their algebras, and the basics for equation systems. We show how to implement term algebras over a signature without resorting to general inductive constructions (currently not allowed in UniMath) still retaining the computational nature of the definition. We prove that our single sorted ground term algebras are instances of homotopy W-types. From this perspective, the library enriches UniMath with a computationally well-behaved implementation of a class of W-types. Moreover, we give neat constructions of the univalent categories of algebras and equational algebras by using the formalism of displayed categories, and show that the term algebra over a signature is the initial object of the category of algebras. Finally, we showcase the computational relevance of our work by…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Algebra and Logic
