This book is an introduction to programming language theory using the proof assistant Agda. Comments on all matters—organisation, material to add, material to remove, parts that require better explanation, good exercises, errors, and typos—are welcome. The book repository is on GitHub. Pull requests are encouraged. There is a private repository of answers to selected questions on github. Please co