Unimath 中的通用代数 (Universal Algebra in UniMath)

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.

翻译：我们在最近开发UniMath校对助理通用代数图书馆时介绍了最新的最新情况。这里讨论的代码涉及多组签名及其代数,以及等式系统的基本原理。此外,我们通过使用显示类别的形式主义,对相应的单项分类进行了整洁的构建,并表明签名的代数一词是该类别的初始对象。除了正式化外,我们还思考了方法原则 -- -- 其依据是系统内常规化程序可评价我们基本建筑的理念 -- -- 引导我们的编码风格,并表明这条路径确实可以通过绘制简单的例子来实际操作。