About this project

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). 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:

• Matteo Cusin

These helped to substantially improve the presentation of this course. Furthermore, feedback of the following persons was influential and greatly appreciated:

• Fredrik Nordvall Forsberg

Open source dependencies

This interactive Agda tutorial builds on awesome free software projects:

The confetti animation is by Elias Ruiz Monserrat.

Similar projects for other languages

• Holbert
• Lean Game Server
• Rocq interactive online system

Working locally

In case you prefer to work with a local Agda installation, there is an archive of all Agda code.

It is also possible to self-host Let’s play Agda.

Backing up your data

• For the interactive Agda elements of this project, you are connected to an container including Agda running on a server of mine. This container is ephemeral, your Agda code is not permanently stored on the server.

• Instead, your solutions to Agda exercises are only 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.