Polarity Problems and the Semantics of Directed Type Theory
Jacob Neumann
University of Nottingham
Abstract:
The goal of Directed Type Theory is to replace the symmetric identity types characteristic of Martin-Löf Type Theory with asymmetric "Hom-types", which equip the types of the theory with the structure of a category. However, since the symmetry of identity is a theorem of MLTT (not an axiom), great care must be taken to ensure that one's directed type theory cannot still prove symmetry, i.e. that it is indeed directed. A natural approach to designing directed type theories is by giving semantics for the theory in the category of categories, and extracting syntax from the semantics.
In this talk, I'll outline the syntax (and category-theoretic semantics) of directed type theory given in my forthcoming PhD thesis. The main idea is to adapt Hofmann and Streicher's groupoid model of (undirected) type theory to the category model of directed type theory. To transport the groupoid model definitions into the category model, we must solve a variety of "polarity problems", where annotations of co-, contra-, iso-, and di-variance have to be made explicit in the syntax of the theory. For instance, we'll need a way to annotate the domain, A, of the function type A-->B as "negative" and its codomain, B, as "positive". I'll detail which polarity problems which have been given satisfactory solutions, and which ones require further work.
This talk is based on joint work with Thorsten Altenkirch.