Universal Algebra in UniMath
Gianluca Amato, Marco Maggesi, Maurizio Parton, Cosimo Perini Brogi
TL;DR
The library for universal algebra in the UniMath framework dealing with multi-sorted signatures, their algebras and the basics for equation systems is presented and it is proved that the authors' single sorted ground term algebras are instances of homotopy W-types.
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.