This is great for me for a completely auxiliary reason, which is that I wanted to know whether this was just gonna be a book about programming Fibonacci numbers into types or some ish... and in some ways it's kinda worse, at chapter 9 you are still proving that different takes on x→x+1 are the same. (But using rewrite rules seems kinda interesting in the abstract I guess.)
This series of books has always been aimed at people who want to implement the underlying systems. If you’re more interested in the application side of dependent types you might like the book Functional Programming in Lean by the same author, which is freely available online!
