Preferred link to see these lecture notes

Download the Agda files as a zip file

How to install Agda 2.6.2.2

Agda manual

Lecture Notes

• Lectures 1─3 delivered by Martín Escardó

  1. Introduction to Agda, dependent types and dependent functions covers (part of) the introduction to Agda notes.
  2. Basic MLTT Types covers the empty type, unit type, binary type, sum types, binary sums and propositions-as-types notes.
  3. Identity types, Σ-types and universes covers the binary sums, the identity type and equality in sums notes.

• Lectures 4─6 delivered by Dan Licata

  4. Intro to higher inductive types
  5. Dependent elimination principles for HITs
  6. Calculating the fundamental group of the circle

Exercise Sheets

Auxiliary files

Advanced further reading

1. Introduction to Homotopy Type Theory and Univalent Foundations (HoTT/UF) with Agda.

HoTTEST School github repository