There are times when some new theory comes along that just seems “right,” regardless of whether one can immediately see applications. The link between homotopy theory and identity types in Martin-Löf type theory has convinced many (including me) that it is one of those theories. Unfortunately, it requires quite a lot of background (dependent type theory, homotopy theory, and category theory) to properly understand. Thankfully, the main idea is simple: not all identities between terms are the same, and some identities in particular may have more computational content than others. Statements more precise than this immediately get rather technical.

Of course, such an idea might have turned out to be entirely fanciful, at least until models were found. While others broke that ground, the authors here present new models, in terms of topological spaces and simplicial sets. More importantly, they present a cogent categorical framework and a set of categorical tools that allow one to much more easily identify new models.

The paper is extremely well written, especially considering the technical difficulty and depth of the material. The authors spend considerable time explaining the main ideas and intuitions, and even point out what their work does not achieve.

One interesting technical aspect is the use of Moore paths in their topological models. Disappointingly, no reference is associated with this. I found the presentation of dependent type theory amusingly sloppy. If the authors had formalized all of their work in a proof assistant, like Coq, they surely would have chosen a different presentation of this material. Hopefully, one day formal papers will be written using formal tools.

This paper is really written for experts, whereas I’m just a highly interested bystander with almost enough of the right background to follow what is going on. In fact, the biggest barrier is the notation, which is likely standard but is not fully explained. All experts should read this paper. Those looking for an introduction to the topic should look elsewhere before coming back to it.