Agda Universal Algebra Library，第2部分：结构
The Agda Universal Algebra Library, Part 2: Structure
摘要：
Agda Universal Algebra Library（UALib）是我们开发的类型和程序（定理和证明）库，用于使用Agda程序设计语言和证明助手形式化依赖类型论中的通用代数基础。UALib包含了来自泛代数、方程逻辑和模型理论的大量定义、定理和证明，并提供了许多例子，展示了归纳和依赖类型在表示和推理数学结构和方程理论方面的能力。在本文中，我们描述的类型和证明的UALib涉及同态，项，和子代数。
英文摘要：
The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof assistant. The UALib includes a substantial collection of definitions, theorems, and proofs from universal algebra, equational logic, and model theory, and as such provides many examples that exhibit the power of inductive and dependent types for representing and reasoning about mathematical structures and equational theories. In this paper, we describe the the types and proofs of the UALib that concern homomorphisms, terms, and subalgebras.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
