This is PLFA book with all code snippets rewritten in Arend.
The book is a collection of markdown files, you can read it right here on GitHub. If you want to interact with the code snippets, clone the repo and open plfa module in IntelliJ IDEA with Arend plugin installed. You may also need the dev version of the arend-lib, just clone it and put next to the repo location.
Part 1: 10/10 sections completed.
Part 2: 1/11 sections completed.
Part 3: 0/5 sections completed.