Learn the Agda basics in three 2-hour sessions.
This Agda tutorial was constructed by Jesper Cockx and is presently maintained by Andreas Nuyts as part of a CS master course titled "Formal Systems and their Applications" at KU Leuven, Belgium. We decided to make it public after receiving comments that there aren't so many quick Agda tutorials out there.
All agda code is currently tuned for Agda 2.5.3 and the Agda standard library v0.14.
It is assumed you use emacs with agda-mode as your IDE. Users may wish to put the .emacs file in their homefolder.