Acknowledgements

The authors acknowledge support by Tamkeen under the NYUAD Research Institute grant CG008.

mvrnote: summer students mvrnote: other people who I sent it to, e.g. fowler

Content and exercises were adapted from many sources, in particular:

• The cubical Agda library by Anders Mörtberg, Felix Cherubini, Evan Cavallo, Axel Ljungström and others
• The 1lab by Amélia Liao, Astra Kolomatskaia, Reed Mullanix and others
• The Cubical Agda tutorial at the HoTTEST Summer School 2022 by Anders Mörtberg
• The cubicaltt tutorial by Anders Mörtberg
• mvrnote: agda-unimath
• Cubical Synthetic Homotopy Theory by Anders Mörtberg and Loïc Pujet
• Introduction to Univalent Foundations of Mathematics with Agda by Martín Escardó
• Introduction to Homotopy Type Theory by Egbert Rijke
• mvrnote: https://www.andrej.com/zapiski/ISRM-LOGRAC-2022/00-introduction.html https://github.com/danelahman/lograc-2022
• mvrnote: https://ulrikbuchholtz.dk/mgs2024-synthetic-homotopy-theory.pdf

The website is built using mdbook, together with some build scripts adapted from the agda-unimath project. Inline code is linked to its definition by a method adapted from the 1lab.