There's even a page in the Idris 2 docs with updates to the book for Idris 2 -- https://idris2.readthedocs.io/en/latest/typedd/typedd.html https://idris2.readth

There's even a page in the Idris 2 docs with updates to the book for Idris 2 -- https://idris2.readthedocs.io/en/latest/typedd/typedd.html https://idris2.readthedocs.io/en/latest/typedd/typedd.html The book is otherwise still totally relevant for Idris 2 and is a great read & introduction to dependent types.