Resources on Agda

Agda is to Coq as Arch is to Ubuntu.

Quick Links

• List of unicode symbols URL
  • M-x and agda-input-show-translations to see the full list,
  • M-x and quail-show-key to query the character under the cursor.
• Agda Reference URL
• GNU Emacs Reference Card (keyboard shortcut cheat sheet) URL
  • Ctrl-, and Ctrl-. do not work in terminal Emacs.
  • Using evil-mode is a good idea, though there are some conflicts with agda-mode in keyboard shortcut.

Keyboard Shortcut Cheat sheet

General,

• C-c C-d: query the type of an expression
• C-c C-n: evaluate an expression (normalize)
• C-c C-l: type check (load)

Jumping between holes,

• C-c C-f: next hole
• C-c C-b: previous hole

Inside a hole,

• C-c C-c: case split a hole
• C-c C-r: refine a hole
• C-c C-a: try to find the solution automatically
• C-c C-,: query the information type about the hole
• C-c C-.: deduce the type of an expression when filled in the hole
• C-c C-Space: check the type inside the hole and replace if compatible

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