About this project#
About this version#
This is a static rebuild of Let’s play Agda, the interactive Agda tutorial created by Ingo Blechschmidt (University of Antwerp) for a 2025 course at the University of Padova organized by Milly Maietti; see the original site and the original repository. The text and the Agda code of the tutorial are the work of the original author and of the contributors named below, and are available under the CC BY-SA license. This version shows them as a static website whose Agda editor runs in your browser (source code of this version). The sections below describing this site’s technology have been updated for this version; the credits are those of the original.
Credits#
Over the years, the structure and contents of this course have been shaped by and greatly benefited from feedback of participants at
- the Chaos Communication Congress (2018, 2019, 2023, 2024),
- the Curry Club Augsburg (2019, 2021),
- two Dagstuhl meetings (2021, 2024),
- the 2022 ALGAR summer school,
- the Proof and Computation autumn school (2022, 2023, 2024),
- two minicourses at the University of Verona (2022, 2024)
– and in particular by the students at the University of Padova (2020, 2021, 2022, 2023, 2024, 2025, 2026). It was set in motion by a course of Martín Escardó at the 2018 installment of Proof and Computation, where I have learned Agda with help from Anja Petković Komel and later Matthias Ritter.
Pull requests were contributed by:
- Taylor Belcher
- Matteo Cusin
- @joha2
- Maja Kądziołka
These helped to substantially improve the presentation of this course. Furthermore, feedback of the following persons was influential and greatly appreciated:
- Timur Aminev
- Martin Ceresa
- Fredrik Nordvall Forsberg
- Johannes Hartung
- Jacopo Piccione
- Alessandro Rizzi
- Noon van der Silk
Open source dependencies#
This interactive Agda tutorial builds on awesome free software projects:
- Agda itself, which runs in your browser as WebAssembly thanks to the Agda Web project and the Agda Language Server,
- Visual Studio Code for the Web (Code - OSS),
- agda-mode for VS Code by Ting-Gian Lua, and the ALS WASM Loader by Andy Pan,
- the cubical library.
Press here for a confetti animation.
Similar projects for other languages#
Working locally#
In case you prefer to work with a local Agda installation, there is an archive of all Agda code.
This tutorial is a static website; its repository contains everything needed to build and host it yourself.
Backing up your data#
The interactive Agda elements of this project run in your browser. There is no server involved, and your Agda code never leaves your computer.
Your solutions to Agda exercises are stored in your browser’s local storage. This storage is in principle permanent but in practice prone to be cleared, for instance when working in your browser’s private mode or when deleting “application data” of web sites. Hence you might want to periodically download your solutions for safekeeping.
You can import backups by clicking here. This will merge the backup’s contents with the local storage.
Streak#
As soon as you have started filling in your first hole, a small calendar will appear in the lower left corner below the navigation. This calender allows you to monitor your progress. Like your Agda code, this activity log is only stored in your browser’s local storage.
Days on which you have been playing
Days on which you have been resting
Days on which you have been inactive
To better match night owls, a day is defined as ending at 5 am in the morning. For the case that this is useful to you, also your longest streak of continuous day-after-day activity is computed. Up two resting days in each 7-day time span do not interrupt a streak.
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.