## 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.