Introduction to Type Theory

Introduction to Type Theory - University of Verona

This page will collect installation info, lecture notes, and further materials as the seminar progresses.

Install Agda

Please install Agda following the instructions:
Agda documentation
Make sure that the standard library is installed!

Tip: Agda works well with either Emacs (with agda-mode) or Microsoft Visual Studio Code (with the Agda extension). Choose whichever editor you prefer.

Lecture Notes

The lecture notes may be updated as the seminar evolves. Always use the link below for the latest version:

Latest PDF: Tao of Types (Draft)

Further Material