Cubical Type Theory

Add to your list(s) Download to your calendar using vCal

• Ian Orton (University of Cambridge)
• Friday 29 April 2016, 11:15-12:15
• Rainbow Room (FS07), Computer Laboratory.

If you have a question about this talk, please contact Ian Orton.

In homotopy type theory (HoTT) we interpret equalities as paths. What does this actually mean? What are paths and what can we do with them? Cubical type theory [1] is a formal system that allows us to reason about paths by introducing an abstract interval object into the type theory. By adding extra structure we can show that these paths have all the usual properties of identity types and more. In particular they allow us to prove the principle of function extensionality, something that most existing type theories are unable to do. Adding yet more structure allows us to obtain a computational interpretation of Voevodsky’s univalence axiom.

In this talk I will introduce cubical type theory in stages. Starting with “vanilla” dependent type theory (without identity types) I will follow a pattern of: adding something to the type theory, explaining why we don’t have identity types yet and repeating until we do.

Specifically, I will show that by simply adding an interval object to dependent type theory we get a notion of path satisfying many of the properties that we expect of identity types (e.g. reflexivity, symmetry, congruence). Then I will describe some of the shortcomings of these paths (we cannot prove that they are transitive or derive a notion of transport) and introduce some additional structure to fix these problems. Finally I will explain why, after all this work, we still don’t quite have the identity types that we all know and love, and how we can fix this using an idea of Andrew Swan.

[1] C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. Preprint, December 2015.

This talk is part of the Logic & Semantics for Dummies series.

This talk is included in these lists:

• Logic & Semantics for Dummies
• Rainbow Room (FS07), Computer Laboratory
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.