For anyone wondering if the Idris book works with v2, I found this [0]. Some code examples in the book need adjustment to work in Idris 2. The Book is great fun.

https://idris2.readthedocs.io/en/latest/typedd/typedd.html#t...