Hacker News new | ask | show | jobs
by ek 4571 days ago
The book on Homotopy Type Theory is quite readable even though the developments are quite new. The purpose of the book is to get the material into the hands of as many as it may be useful to as soon as possible.

I would argue that the book is at least as useful as Categories for the Working Mathematician or Barendregt's Lambda Calculus are likely to be for your typical software engineer interested in functional programming. To be clear, someone interested only in learning how to program in functional languages is probably not going to get very much from either of those books, which are respectively an extremely technical mathematical text on topics in category theory, and a heavily logic-oriented, mathematical presentation of the lambda calculus and derivatives thereof. Not much of the material in either book would be directly applicable to the practice of software engineering using functional languages, but someone with a deeper interest would find them useful and interesting, and I think the same holds for the HoTT book. At the very least, as the other commenter alluded to, a novice reader would probably be able to glean a nice understanding of Martin-Löf dependent type theory from the first chapter.