A very mind-blowing and challenging book about Types.
The strange loop talk and my own interview of the authors might give some sense of what it's all about. There is also some interesting work online showing how the language used in the book can be created.
I was at that talk by David which is the first link. Highly recommended watch, he is such a good presenter. The way he went full circle there and had the room in raucous applause at the end was something I never forgot.
The Strange Loop talk was very enjoyable. You are a gifted public speaker. And I just want to say that I am excited to read your book on Lean in full, too!
The strange loop talk and my own interview of the authors might give some sense of what it's all about. There is also some interesting work online showing how the language used in the book can be created.
https://www.youtube.com/watch?v=VxINoKFm-S4
https://corecursive.com/023-little-typer-and-pie-language/
https://davidchristiansen.dk/tutorials/nbe/