Universal Algebra in UniMath
Gianluca Amato, Marco Maggesi, Maurizio Parton, Cosimo Perini Brogi
TL;DR
This paper discusses the development of a formal framework for Universal Algebra within the UniMath proof assistant, leveraging Univalent Mathematics to formalize algebraic structures and their invariants.
Contribution
It introduces a novel approach to formalizing Universal Algebra in UniMath, emphasizing the use of univalent foundations to isolate algebraic invariants.
Findings
Initial implementation of Universal Algebra in UniMath
Framework for formalizing algebraic structures modulo isomorphism
Potential for rigorous formal proofs in algebraic theory
Abstract
We present an ongoing effort to implement Universal Algebra in the UniMath system. Our aim is to develop a general framework for formalizing and studying Universal Algebra in a proof assistant. By constituting a formal system for isolating the invariants of the theory we are interested in -- that is, general algebraic structures modulo isomorphism -- Univalent Mathematics seems to provide a suitable environment to carry on our endeavour.
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
TopicsLogic, programming, and type systems · semigroups and automata theory · Advanced Algebra and Logic