file.pdf (413.36 kB)

# 2-Dimensional Directed Dependent Type Theory

journal contribution

posted on 2006-10-01, 00:00 authored by Daniel R. Licata, Robert HarperThe 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.