About this project
Mention streak…
Credits
Open source dependencies
This interactive Agda tutorial builds on awesome free software projects:
Similar projects for other languages
Download
In case you prefer to work with a local Agda installation, there is an archive of all Agda code.
Unicode symbols
Agda’s community is big on Unicode, helping us to notationally mimic
blackboard mathematics. On this webpage, you can hover over special
symbols in Agda fragments to learn how they can be input. Many LaTeX
commands work, for instance \alpha will produce a Greek
α.
Here is a list of Unicode symbols used in this course.