Universal Algebra in UniMath
University of Florence
Abstract:
We present recent updates in our development of a library for
Universal Algebra in the UniMath proof assistant. The code here
discussed, concerns multi-sorted signatures and their algebras,
along with the basics for equation systems. Moreover, we give
neat constructions of the corresponding univalent categories by
using the formalism of displayed categories, and show that the
term algebra over a signature is the initial object of the
category.
Besides the formalization, we reflect on the methodological
principles – based on the idea of evaluability of our elementary
construction by the built-in normalization procedure of the
system – leading our coding style, and show that this path is
practicable indeed by sketching simple examples.