Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom
(Joint work with Cyril Cohen, Thierry Coquand and Simon Huber)
Homotopy type theory is an extension of dependent type theory inspired by connections to abstract homotopy theory. This connection was discovered, among others, by Fields medalist Vladimir Voevodsky and from it a new axiom, called the univalence axiom, was added to type theory. This axiom provides extensionality principles, for instance function extensionality and the possibility to transport properties between isomorphic structures. One of the open problems in this new field is whether this axiom has computational content. In this talk I will discuss an extension to dependent type theory, called cubical type theory, which allows the user to directly argue about higher dimensional cubes representing equality proofs. This system provides new ways to reason about equality in type theory, in particular the univalence axiom is provable in the system which hence gives a computational justification for it.
Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:30 | |||
14:00 50mTalk | Invited Talk -- Cubical Type Theory: a constructive interpretation of the univalence axiom TTT Anders Mörtberg Inria | ||
14:50 20mTalk | Equations: a tool for dependent pattern-matching TTT File Attached | ||
15:10 20mTalk | Coq's Prolog and application to defining semi-automatic tactics TTT File Attached |