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 pull requests big and small, and for answering questions on the Agda mailing list:

For support:

  • EPSRC Programme Grant EP/K034413/1
  • NSF Grant No. 1814460
  • Foundation Sciences Mathematiques de Paris (FSMP) Distinguised Professor Fellowship