论文标题
AGDA中类别理论的形式化
Formalizing of Category Theory in Agda
论文作者
论文摘要
现代数学中类别理论的一般性和普遍性使其成为形式化的常见和有用的目标。然而，由于各种原因，正式化是非常具有挑战性的。 AGDA目前（即2020年）没有标准的类别理论形式化。我们记录了解决这一难题的工作。正式化揭示了许多潜在的设计选择，我们提出，激励和解释我们选择的选择。特别是，我们发现来自标准教科书中发现的替代定义或替代证明可能是有利的，并且“ Fit” Agda的类型理论更加顺利。在标准教科书中，某些定义被认为是等效的，这些定义是做出不同的“宇宙级别”假设的，其中一些比其他定义比其他定义更重要。我们还密切关注工程问题，以便图书馆与AGDA自己的标准库很好地集成，并与AGDA中尽可能多的支持类型理论兼容。
The generality and pervasiness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not have a standard, working formalization of category theory. We document our work on solving this dilemma. The formalization revealed a number of potential design choices, and we present, motivate and explain the ones we picked. In particular, we find that alternative definitions or alternative proofs from those found in standard textbooks can be advantageous, as well as "fit" Agda's type theory more smoothly. Some definitions regarded as equivalent in standard textbooks turn out to make different "universe level" assumptions, with some being more polymorphic than others. We also pay close attention to engineering issues so that the library integrates well with Agda's own standard library, as well as being compatible with as many of supported type theories in Agda as possible.
