Cubical Intepretations of Type Theory

Abstract

The interpretation of types in intensional Martin-Löf type theory as spaces and their equalities as paths leads to a surprising new view on the identity type: not only are higher-dimensional equalities explained as homotopies, this view also is compatible with Voevodsky's univalence axiom which explains equality for type-theoretic universes as homotopy equivalences, and formally allows to identify isomorphic structures, a principle often informally used despite its incompatibility with set theory.

While this interpretation in homotopy theory as well as the univalence axiom can be justified using a model of type theory in Kan simplicial sets, this model can, however, not be used to explain univalence computationally due to its inherent use of classical logic. To preserve computational properties of type theory it is crucial to give a computational interpretation of the added constants. This thesis is concerned with understanding these new developments from a computational point of view.

In the first part of this thesis we present a model of dependent type theory with dependent products, dependent sums, a universe, and identity types, based on cubical sets. The novelty of this model is that it is formulated in a constructive metatheory.

In the second part we give a refined version of the model based on a variation of cubical sets which also models Voevodsky's univalence axiom. Inspired by this model, we formulate a cubical type theory as an extension of Martin-Löf type theory where one can directly argue about n-dimensional cubes (points, lines, squares, cubes, etc.). This enables new ways to reason about identity types. For example, function extensionality and the univalence axiom become directly provable in the system. We prove canonicity for this cubical type theory, that is, any closed term of type the natural numbers is judgmentally equal to a numeral. This is achieved by devising an operational semantics and adapting Tait's computability method to a presheaf-like setting.