Proof Theory of Homotopy Type Theories by Ulrik Buchholtz (Carnegie Mellon University, USA)

Talk at: FOMUS 2016. For all Talks and more information, slides etc. see: ​Proof Theory of Homotopy Type Theories by Ulrik Buchholtz (Carnegie Mellon University, USA) Abstract: ​It is my opinion that a proposed class of formal systems for the foundations of mathematics needs to be thoroughly understood in terms of interpretations to and from other such systems, with an eye towards answering questions such as 1) what rests on what?, 2) what is needed for what?, 3) how do things fit together?, and 4) how much strength do various principles buy us? In this talk, I shall give an overview about what is known about these questions for systems for homotopy type theory. I shall recall earlier work on the proof theory on type theory and explain how recent work on cubical type theories furthers our understanding. This workshop was organised with the generous support of the Association for Symbolic Logic (ASL), the Association of German Mathematicians (DMV), the