2-Dimensional Directed Type Theory

摘要

Recent work onhigher-dimensional type theoryhas explored connections between Martin-L?f type theory, higher-dimensional category theory, and homotopy theory. These connections suggest a generalization of dependent type theory to account for computationally relevant proofs of propositional equality—for example, takingIdSetA Bto be the isomorphisms betweenAandB. The crucial observation is that all of the familiar type and term constructors can be equipped with a functorial action that describes how they preserve such proofs. The key benefit of higher-dimensional type theory is that programmers and mathematicians may work up to isomorphism and higher equivalence, such as equivalence of categories.In this paper, we consider a further generalization of higher-dimensional type theory, which associates each type with adirectednotion of transformation between its elements. Directed type theory accounts for phenomena not expressible in symmetric higher-dimensional type theory, such as a universe set of sets and functions, and a typeCtxused in functorial abstract syntax. Our formulation requires two main ingredients: First, the types themselves must be reinterpreted to take account ofvariance; for example, a Π type is contravariant in its domain, but covariant in its range. Second, whereas in symmetric type theory proofs of equivalence can be internalized using the Martin-L?f identity type, in directed type theory the two-dimensional structure must be made explicit at the judgemental level. We describe a2-dimensional directed type theory, or2DTT, which is validated by an interpretation into the strict 2-categoryCatof categories, functors, and natural transformations. We also discuss applications of 2DTT for programming with abstract syntax, generalizing the functorial approach to syntax to the dependently typed and mixed-variance case.