UniMath中的泛代数
Universal Algebra in UniMath
AI总结：
该研究在UniMath框架中构建泛代数库，实现无需通用归纳构造的项代数并证明其为同伦W-型实例，构造单值代数范畴且展示项代数的初始性，丰富了UniMath的W-型计算实现。
摘要：
我们提出了UniMath框架中的泛代数库，处理多类签名、其代数及方程组基础。我们展示了如何在签名上实现项代数，无需借助通用归纳构造（目前UniMath不允许），同时保留定义的计算性质。我们证明单类基项代数是同伦W-型的实例。从这一视角，该库为UniMath丰富了计算性良好的一类W-型实现。此外，我们利用展示范畴的形式化方法，简洁构造了代数和等式代数的单值范畴，并证明签名上的项代数是代数范畴的初始对象。最后，我们通过概述代数和命题逻辑中的一些基本示例，展示了工作的计算相关性。
英文摘要：
We present our library for Universal Algebra in the UniMath framework dealing with multi-sorted signatures, their algebras, and the basics for equation systems. We show how to implement term algebras over a signature without resorting to general inductive constructions (currently not allowed in UniMath) still retaining the computational nature of the definition. We prove that our single sorted ground term algebras are instances of homotopy W-types. From this perspective, the library enriches UniMath with a computationally well-behaved implementation of a class of W-types. Moreover, we give neat constructions of the univalent categories of algebras and equational algebras by using the formalism of displayed categories, and show that the term algebra over a signature is the initial object of the category of algebras. Finally, we showcase the computational relevance of our work by sketching some basic examples from algebra and propositional logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
