00:00:00 / 00:00:00

Towards a Syntax for Cubical Type Theory 1/2

By Thorsten Altenkirch

Appears in collection : 2014 - T2 - Semantics of proofs and certified mathematics

One of the key problems of Homotopy Type Theory is that it introduces axioms such as extensionality and univalence for which there is no known computational interpretation. We propose to overcome this by introducing a Type Theory where a heterogenous equality is defined recursively and equality for the universe just is univalence. This cubical type theory is inspired by Bernardy and Moulin's internal parametricity and by Coquand, Bezem and Huber's cubical set model. This is ongoing work with Ambrus Kaposi at Nottingham.

Information about the video

  • Date of publication 19/05/2014
  • Institution IHP
  • Format MP4

Last related questions on MathOverflow

You have to connect your Carmin.tv account with mathoverflow to add question

Ask a question on MathOverflow




Register

  • Bookmark videos
  • Add videos to see later &
    keep your browsing history
  • Comment with the scientific
    community
  • Get notification updates
    for your favorite subjects
Give feedback