A Formal Logic for Formal Category Theory (Extended Version)

TL;DR

This paper introduces a specialized type theory that formalizes category theory concepts, ensuring functoriality and naturality by construction, simplifying key proofs like Yoneda lemma within a rigorous logical framework.

Contribution

It develops a domain-specific type theory for category theory that guarantees functoriality and naturality, simplifying proofs and extending to enriched and internal categories.

Findings

Type theory axiomatizes categories, functors, profunctors, and natural transformations.

All category-theoretic proofs become straightforward type-theoretic proofs.

The type theory is sound and complete for models in virtual equipments.

Abstract

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.