So far we have seen just one way to say that two things are the same: judgemental equality. Judgemental equality pertains to the expressions of the language; when two expressions are judgemental equally, then they unavoidably describe the same mathematical object, but we might consider the converse: if two expressions describe the “same” mathematical object, are the expressions themselves judgementally equal?
One way to test this proposition is to consider the extension of our type theory with identification types u=_A v for u,v:A whose elements represent evidence that u and v describe the same mathematical object. This is subtly different from the equality judgement u\equiv v:A in an important way, putting aside the fact that one is a judgement and other is a type:
- The equality judgement u\equiv v:A asserts that u and v are the same description of an element of A.
- An element w:u=_Av witnesses that u and v describe the same mathematical object, rather than that they are the same description.
In real life, it can happen that two different expressions describe the same thing; for example, it is often pointed out that the “morning star” and the “evening star” both describe the planet Venus—although examples like this can be troublesome since one can always force the referents to be distinct again by arguing that (e.g.) one expression describes Venus in the morning, and the other describes Venus in the evening, etc.
In much of mathematics, it was considered that the converse proposition (that any two descriptions of the same object are themselves the same) was perfectly natural and could therefore be included as a formal rule of dependent type theory that relates judgmental equality with identification types. This rule was called equality reflection. But in the final two decades of the 20th Century, three different objections to equality reflection emerged:
- A philosophical objection. Around 1986, Per Martin-Löf re-analysed the philosophical foundations of dependent type theory and came to the conclusion that equality reflection was not justified in a philosophical sense. Martin-Löf’s philosophical objection to equality reflection did not rise to the level of a mathematical objection: indeed, equality reflection is consistent with traditional mathematics.
- A practical objection. During the 1980s and 1990s, efficient algorithms for automatically checking the judgements of dependent type theory were developed (including those underlying Rocq, Agda, and Lean), but these algorithms rely on the omission of equality reflection; indeed, the judgements of type theory with equality reflection are known to be undecidable.
- A mathematical objection. Toward the end of the 1990s, the late Martin Hofmann and Thomas Streicher discovered a mathematical objection to equality reflection: a model of type theory based on groupoids in which there can be multiple mathematically distinct ways to identify two objects as “the same”, which contradicts equality reflection; moreover, the notion of sameness that interpreted the identification type in this model was closer to everyday mathematical usage than that of the standard model in set theory. Although equality reflection remains consistent, there was finally compelling evidence that equality reflection was warping our perception of mathematics in a harmful way.
The three objections above are not insurmountable, but they are strong enough together that intensional type theory (which is type theory without equality reflection) has become a leading point of view. Intensional type theory alone does not, however, take advantage of the possibilities suggested by Hofmann and Streicher’s groupoid interpretation; in this module, we consider an extension of intensional type theory called homotopy type theory that solves these problems and more.