Universal Algebra in UniMath
Logic in Computer Science
2024-12-11 v1
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.
Keywords
Cite
@article{arxiv.2007.04840,
title = {Universal Algebra in UniMath},
author = {Gianluca Amato and Marco Maggesi and Maurizio Parton and Cosimo Perini Brogi},
journal= {arXiv preprint arXiv:2007.04840},
year = {2024}
}
Comments
Accepted at the HoTT/UF 2020 workshop