Wen Kokke, Jeremy Siek, Philip Wadler


Thank you to:

  • The inventors of Agda, for a new playground.

  • The authors of Software Foundations, for inspiration.

A special thank you, for inventing ideas on which this book is based, and for hand-holding:

  • Conor McBride

  • James McKinna

  • Ulf Norell

  • Andreas Abel

For a note showing how much more compact it is to avoid raw terms:

  • David Darais

For support:

  • EPSRC Programme Grant EP/K034413/1

  • NSF Grant No. 1814460

  • Foundation Sciences Mathematiques de Paris (FSMP) Distinguised Professor Fellowship


This work is licensed under a Creative Commons Attribution 4.0 International License. Some changes were made to the original version in order to adapt its contents to nextjournal.