论文标题
形式类别理论的形式逻辑（扩展版）
A Formal Logic for Formal Category Theory (Extended Version)
论文作者
论文摘要
我们为类别理论中的构造和证明提供了特定领域的类型理论。类型理论公理化了类别，函子，分解器和自然变换的广义形式的概念。该类型理论对标准谓词逻辑施加有序的线性限制，该逻辑确保类别之间的所有功能都是函数函数，所有关系都是分配的，并且所有转换都是自然而然的构造，而无需单独的证据。重要的类别理论证明，例如Yoneda引理和共同YONEDA引理，成为有关单位，张量和（有序的）功能类型之间关系的简单类型理论证明，并且可以被认为是谓词逻辑中定理的改进。对于虚拟设备中的分类模型，类型理论是合理的，并且是完整的，该模型既模拟内部和丰富的类别理论。虽然我们类型理论中的证据看起来像是基于标准的论点，但句法学科确保所有证明和构造也将其延续到丰富和内部设置。
We present a domain-specific type theory for constructions and proofs in category theory. The type theory axiomatizes notions of category, functor, profunctor and a generalized form of natural transformations. The type theory imposes an ordered linear restriction on standard predicate logic, which guarantees that all functions between categories are functorial, all relations are profunctorial, and all transformations are natural by construction, with no separate proofs necessary. Important category-theoretic proofs such as the Yoneda lemma and Co-yoneda lemma become simple type-theoretic proofs about the relationship between unit, tensor and (ordered) function types, and can be seen to be ordered refinements of theorems in predicate logic. The type theory is sound and complete for a categorical model in virtual equipments, which model both internal and enriched category theory. While the proofs in our type theory look like standard set-based arguments, the syntactic discipline ensure that all proofs and constructions carry over to enriched and internal settings as well.
