Type Theory

Univalent type theory has uncovered new connections between higher dimensional category theory, logic, and computer science. Since its inception, three main strands of research have aimed at deepening and extending this connection.

Model Theory

Soon after introducting the homotopy theoretic interpretation of type theory, Voevodsky, et al, showed that there was indeed a model of the theory in simplicial sets, which additionally satisfied his univalence axiom. A consequence is that theorems proved internally to type theory are in fact theorems about homotopy types in the traditional mathematical sense of the word.

Various other authors have extended these results, showing that we can obtain univalent models in many other categories.

Computational Theory

In practice, using univalent type theory has involved adding axioms to existing type theories in order to access higher dimensional information. The univalence axiom itself, but also higher inductive types must be added to proof assistants by hand.

From a type-theoretic perspective, this situation is less than ideal, since adding axioms to type theory breaks its computational interpretation: a proof assistant is unable to reduce a term which contains an instance of an axiom, since the simple addition of an axiom does not explain its reduction behavior.

The cubical type theory of Coquand, Cohen, Huber, and Mortberg, aims at solving this problem.

Coherence Theory

As with most investigations into higher category theory, problems of coherence have cropped up almost from the beginning. From an internal perspective, the types of univalent type theory behave like infinity groupoids, coherent at all levels. But we cannot describe internally what coherence means, since doing so requires us to write down types with infinitely many constructors.

Most work on this problem has focused on finding a reasonable internal definition of simplicial type. The main idea is that axiomatizing such an object would allow us to speak of main other kinds of higher coherent objects such as internal groupoids and (infinity, 1)-categories. So far, however, no simple solution to this problem has been found.