Homotopy Type Theory and Hedberg's Theorem
Intensional Martin-Loef Type Theory, the foundation of systems such as
Coq and Agda, is currently experiencing a revolution. One of its
subtleties are equality types: Seemingly among the simplest inductive
types, are they probably one of the hardest to understand.
In recent years, the justification for a certain axiom, guaranteeing the
uniqueness of equality proofs, has been questioned. It turned out that,
after dropping it, type theory has a model in a field that is
well-researched by mathematicians. At the same time, many desirable
properties of type theory can be obtained, some of which seemed to be
impossible before.
In this talk, I provide an introduction to this interesting development,
usually referred to as "Homotopy Type Theory". Further, I demonstrate
generalizations of Hedberg's theorem as an example of reasoning in the
"new" system, based on joint work with Thorsten Altenkirch, Thierry
Coquand and Martin Escardo.