Universal Algebra in UniMath (preprint) Presented at Workshop on Homotopy Type Theory and Univalent Foundations 2020

We present an ongoing effort to implement Universal Algebra in the UniMath system [12]. 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. After introducing the classical definition of signature, we give the related formalization of the category of algebras using the notion of a displayed category over the univalent category of sets; in this way, we easily obtain a proof that the corresponding total category of algebras is univalent. Our formalization also includes the notion of equations and varieties associated with a signature; as for the category of algebras, we construct the category of varieties over a given signature, and prove in a modular way that it is univalent by using the formalism of displayed categories. Our code is publicly available from https://github.com/amato-gianluca/UniMath. The revision discussed in this paper is tagged as hott-uf-2020.