Rating is available when the video has been rented.
This feature is not available right now. Please try again later.
Published on Nov 19, 2014
On 9 Nov 2014, at Homotopy Type Theory Workshop (7-10 Nov 2014, Mathematical Institute, University of Oxford)
Abstract: In this talk, I will describe work in progress (joint with Guillaume Brunerie) on a cubical syntax for type theory. The goal of the work is to provide a syntactic type theory where the computational aspects of the cubical sets model by Bezem, Coquand, and Huber can be expressed. I will describe a "boundaries-as-terms" cubical type theory, where the basic judgement is "the term u is an n-cube in the type A, together with its boundary", and the cubical operations (faces, degeneracies, symmetries, and diagonals) can be applied to any term. This syntax permits a clean formulation of the computation rules for Kan fillings in Pi, Sigma, and identity types. Moreover, diagonals support the computation rules for higher inductive types. The most salient open issue is how to define the Kan fillings for the universe and for univalence; I would welcome collaboration on this after the talk