Resources on Agda

Feb 6 2023 · LastMod: Mar 2 2023

Agda is to Coq as Arch is to Ubuntu.

Keyboard Shortcut Cheat sheet


Jumping between holes,

Inside a hole,

Tutorials and lectures (that I found most useful)

  1. (Notes) Introductory level: course for master students at ELTE Eötvös Collegium in Budapest by Péter Diviánszky and Ambrus Kaposi URL
    • Some errors in, to say the least, the ‘Emacs Usage’ section, e.g. \bN for $\mathbb{N}$ instead of \bn.
  2. (Videos, fast-paced, HoTT-oriented) HoTTEST Summer School 2022, online lectures by assorted instructors. URL
  3. (Videos, slow-paced, mathematics-oriented) Peter Silinger’s lectures URL
  4. Programming Language Foundations in Agda, namely PLFA. Note that the leading codeblocks in each chapters should be ignored.

PLFA Solutions (selected)

Solutions are encryped, in accordance to what is written here

  1. Naturals
  2. Induction
  3. Relations
  4. Equalities