Why is it so difficult to introduce type theory to the rest of us?
One episode in the Beginning Mathematical Logic Study Guide which I must radically revise in the next edition is the final section on type theories, which was tacked on almost as an afterthought. But it will, indeed, take quite a bit of work to organize a better overview of what is a messy area, and devotees of varieties of type theory are not always the clearest of advocates to help us along.
Egbert Rijke has an Introduction to Homotopy Type Theory coming out soon with CUP. This is a textbook aimed at quite a wide readership; “it introduces the reader to Martin-Löf’s dependent type theory, to the central concepts of univalent mathematics, and shows the reader how to do mathematics from a univalent point of view. … The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed.” Which sounds promising. And a late pre-print can now be downloaded: here’s the link. This may very well be very useful to some readers of this blog, depending on your background. And all credit to Rijke for making his text freely available on the arXiv.
The first part of the book is, as announced, on Martin-Löf’s version of type theory. I’ve dived into this 98 page introduction hopefully. But I can’t, to be honest, say that I have wildly enjoyed the experience — Rijke makes it no easier than others for a conservatively-minded logician to happily find their way in. He acknowledges “Type theory [or at least, type theory of this stripe] can be confusing for people who are new to the subject,” but this means that many of us could do with rather more explanatory chat than we get here. For a small but not insignificant example, right at the outset we are told without further ado that “The expression 𝑎 : 𝐴 is … not considered to be a proposition, i.e., something which one can assert about an arbitrary element and an arbitrary type, but it is considered to be a judgment, i.e., an assessment that is part of the construction of the element 𝑎 : 𝐴.” Is the distinction between a proposition and a judgement transparently clear to you? No. Me neither. (Amusingly, I asked ChatGPT to give a simple explanation of the difference between propositions and judgements in Martin-Löf, and it was a lot clearer. On its first attempt. Though it lost the plot a bit when the question was re-asked.)
Well, meaning is use and all that, and eventually the mists clear somewhat as the notions of proposition and judgement get used later in Rijke. More generally, if you have in fact already encountered a bit of type theory, his explanations will probably serve well for revision and consolidation. But we still await (OK, I still await) a really introductory text on dependent-type-theory-for-old-fashioned-logicians.
The post Why is it so difficult to introduce type theory to the rest of us? appeared first on Logic Matters.
