Episode 3: Dan Licata on Homotopy Type Theory

Posted on by David Christiansen

In our third episode, we dicuss homotopy type theory (HoTT) with Wesleyan University’s Dan Licata. Dan has participated during much of the development of HoTT, having completed his PhD at CMU and having been a part of the Institute for Advanced Study’s special year on the subject. In our interview, we discuss the basics of HoTT, some potential applications in both mathematics and computing, as well as ongoing work on computation, univalence, and cubes.

Reading:

  • The HoTT book is a collaborative effort from the IAS’s Univalent Foundations program. It presents the basics of HoTT, and then demonstrates how a number of different branches of mathematics can be developed within it.
  • Homotopical Patch Theory by Carlo Angiuli, Edward Morehouse, Dan Licata, and Bob Harper is the expanded version of the ICFP paper mentioned in the podcast. This paper applies HoTT to a programmer-relevant topic: Darcs’s patch theory. It can serve as a good introduction to higher inductive types for those whose intuitions are based in code.
  • Dan’s Oxford talk: A Cubical Infinite-Dimensional Type Theory. slides / video
  • Dan’s publications and talks page has a number of papers and presentations on HoTT.
  • Overview of Nuprl: Innovations in Computational Type Theory using Nuprl