Cubical Agda Tutorial

This was written while I was getting up to speed with Cubical Agda.

Quick start

Installing Agda

If you already have Agda installed, great. If not, follow the official instructions. I use brew install agda.

Installing cubical

There are install instructions at https://agda.readthedocs.io/en/v2.6.1/language/cubical.html . Only the paragraph "For detailed install instructions..." is necessary; it amounts to cloning the Cubical repo, building it, and adding it to ~/.agda/libraries and ~/.agda/defaults.

Which file to start with

The first file is File1.agda. Open it up in emacs (or your normal Agda editing environment) and follow it.