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.
I also agree that there is a huge gap in the literature here. Type theory offers an exciting new way of thinking of the entire field of logic, and while there is a lot of material on type theory written for people with computer science backgrounds (e.g., the book by Mimram mentioned by others), I believe there is really no suitable introduction to this material for philosophers.
When one wants to learn not just Martin-Lof type theory but homotopy type theory, it gets even more difficult – unless you really have some sense of how to think like a homotopy type theorist, even Rijke’s book is going to be fairly unintelligible, as he does very little to motivate many of the very complicated constructions and theorems of the book. (I think the original HoTT book is actually better on this front, though it also has limitations from a pedagogical point of view.) I’m definitely not trying to disparage anyone’s efforts here, but in my view a gaping hole in the literature remains even with the appearance of Rijke’s rich and dense book.
I’ve actually taught several courses on type theory here in the philosophy department at the University of Chicago (and am currently teaching a course outlining some of the basics of homotopy type theory), and am in the process of writing and polishing some notes with the goal of producing a monograph introducing type theory (including the basics of homotopy type theory) to philosophers. But this is far from a straightforward task.
Although I think that Egbert’s book is orders of magnitude above the HoTT book in terms of quality and coherency, I do agree with you that people coming to it with a background in traditional logic are going to find the beginning frustrating.
I attended the HoTTEST Summer School program last summer which was an introduction to homotopy type theory as well as formalization in Agda, and in addition to parallel lecture tracks, we used an (almost complete) draft of Egbert’s book as the text. The most frustrating thing that students reported was that between the live lectures on HoTT, the live lectures on Agda, and the book, there were three completely different syntaxes used to describe the same things. Some might argue that seeing the same thing presented three different ways is a good thing, and maybe it is, but only so after you’ve grasped it one way and can compare the new ways to what you understand. The second biggest complaint was that after three weeks, people were able to do the homework assignments but still nobody could articulate what a judgement was.
All of that is just to say, I agree with the criticism that this is not a holy grail for introductions, and that someone looking to get into the subject will probably want something which is easier at the beginning. However, this book is currently, beyond a doubt, the best introduction to HoTT and should be the go-to for anyone who wants to see that side of type theory. I don’t even think the introduction to the mechanics of Martin-Löf type theory is bad, it’s just not as outsider-friendly as it can be. In the guide you could call it a second book on MLTT which summarizes the basics of the theory and then introduces HoTT.
I was reminded of that the other day when I happened to look at the Wikipedia page for Natural deduction and found that type theorists and Martin-Löf fans had been at work; and so it uses “judgement”, explains what a judgement is (I’m not sure how well), has a Proofs and type theory section, and discusses Dependent Type Theory as an example(!)
I’m wanting to learn some Type Theory in part because I have an interest in Proof Assistants. While I haven’t put much effort in yet (I *bought* “The Little Typer”), and age hasn’t been gentle on my cognition, I think it’s going to be quite difficult to let go of my naive Set Theory view of the world. (I’m fortunate that my life is composed solely of the necessary and my hobbies – the point being that I’m just a hobbyist, or worse, a dilettante.) Nonetheless, from my current distance, it just feels so complex, as if all of Mathematics has been embedded in itself, and we must have taken a wrong turn somewhere. I know too little for that to be a judgement, just a little sadness at the possibility of losing the essential, simple, elegance of the foundations as I’ve known them.
I remember the publisher of Saharon Shelah’s Cardinal Arithmetic describing it as a book that “takes a reader with a knowledge of naive set theory to the frontiers of the subject”, as if knowing some elementary set theory was all the background required. L O L
It’s not quite so misleading to describe this Introduction to Homotopy Type Theory as suitable for “students from a wide variety of backgrounds, including mathematics, computer science, and philosophy majors” –undergraduates, without even the standard warning sign, “advanced undergraduates” — or to suggest that “type theory can be confusing for people who are new to the subject, since mathematical training traditionally focuses on sets”.
It is a bit misleading, though. It makes more sense to think of it as a graduate-level text that doesn’t formally require that (but becomes much easier to understand if) the reader has already encountered and worked with simpler forms of type theory. And if mathematical training focusing on sets were the problem, people would find types in ordinary programming languages confusing too, for similar reasons. They don’t. The difficulty isn’t from the difference between types and sets: it’s from the theory part.
Anyway, there’s a different book that looks like it could be much more accessible: PROGRAM = PROOF by Samuel Mimram. It’s self-published, downloadable as PDF, and available here: http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/publications/
Another book that introduces dependent type theory — one perhaps especially suitable for programmers who know some Scheme (or another dialect of Lisp) — is The Little Typer by Daniel P. Friedman and David Thrane Christiansen. I described it like this in a Logic Matters comment a while back: