2-Dimensional Directed Dependent Type Theory

The groupoid interpretation of dependent type theory given by Hofmann and Streicher associates to each closed type a category whose objects represent the elements of that type and whose maps represent proofs of equality of elements. The categorial structure ensures that equality is reflexive (identity maps) and transitive (closure under composition); the groupoid structure, which demands that every map be invertible, ensures symmetry. Families of types are interpreted as functors; the action on maps (equality proofs) ensures that families respect equality of elements of the index type. The functorial action of a type family is computationally non-trivial in the case that the groupoid associated to the index type is non-trivial. For example, one may identity elements of a universe of sets up to isomorphism, in which case the action of a family of types indexed by sets must respect set isomorphism. The groupoid interpretation is 2-dimensional in that the coherence requirements on proofs of equality are required to hold “on the nose”, rather than up to higher dimensional equivalences. Recent work by Awodey and Lumsdaine, Voevodsky, and others extends the groupoid interpretation to higher dimensions, exposing close correspondences between type theory, higher-dimensional category theory, and homotopy theory. In this paper we consider another generalization of the groupoid interpretation that relaxes the symmetry requirement on proofs of “equivalence” to obtain a directed notion of transformation between elements of a type. Closed types may then be interpreted as categories, and families as functors that extend transformations on indices to transformations between families. Relaxing symmetry requires a reformulation of type theory to make the variances of type families explicit. The types themselves must be reinterpreted to take account of variance; for example, a type is contravariant in its domain, but covariant in its range. 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. The resulting 2-dimensional directed dependent type theory, or 2DTT, is validated by an interpretation into the strict 2-category Cat of categories, functors, and natural transformations, generalizing the groupoid interpretation. We conjecture that 2DTT can be given semantics in a broad class of 2-categories, and can be extended to make the higher dimensional structure explicit. We illustrate the use of 2DTT for writing dependently typed programs over representations of syntax and logical systems.