论文标题
Unimath中的环球代数
Universal Algebra in UniMath
论文作者
论文摘要
我们提出了在Unimath系统中实施通用代数的持续努力。我们的目的是开发一个在证明助手中正式和研究普遍代数的一般框架。通过构成一个正式的系统，用于隔离我们感兴趣的理论的不变性 - 也就是说，通用代数结构模型同构 - 单价数学似乎为进行我们的努力提供了合适的环境。
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.
