Cubical Type Theory

Previously, we discussed Homotopy Type Theory, which is an alternative foundation of mathematics with several advantages over ZFC, mainly for computer-assisted proofs. It is based on Martin-Löf’s intuitionistic type theory, but with the idea that types are spaces, terms are points within that space, and that A = B is the space of paths between A and B (viewed as points in a universe U). To accomplish this, recall that there are two extra modifications beyond intuitionistic type theory:

  • Voevodsky’s univalence axiom states that equivalent types are equal, and more specifically that the space of equivalences between two types is equivalent to the space of paths between two types;
  • The introduction of higher inductive types which define not only their elements (vertices) but also paths, 2-cells (paths between paths), and so forth.

An advantage of intuitionistic type theory is that the lack of axioms mean that all proofs of constructive. Including the univalence axiom breaks this somewhat, which is why people have been searching for a way to adapt type theory to admit univalence not as an axiom, but as a theorem.

Cubical type theory was introduced as a constructive formulation which includes univalence and has limited support for certain higher inductive types. A recent paper by Thierry Coquand (after whom the automated theorem-prover Coq is named), Simon Huber, and Anders Mörtberg goes further towards constructing higher inductive types in cubical type theory.

Advertisements
This entry was posted in Uncategorized. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s