Acknowledgements

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

Thank you to all the students who participated in Summer 2023 and Summer 2024, especially those that made it to the end: Eyerusalem Hawoltu Afework, Tasnim Ahmed, Abdullah Alhussni, Omar Al-Khazali, Shaima Al Saeedi, Meriem Aoudia, Mohammed Arham, Desmond Ofori Atta, Fedi Ben Othmen, Rojan Dangol, Gaweed Elmogy, Shaza Elsharief, Narek Galstyan, Rana Gharaibeh, Ziad Hassan, Zyad Yasser Hassan, Ngoc Hoang, Genie Hou, Zurab Jashi, Muhammad Hassan Khan, Himanshi Lalwani, Chunting Liu, Yugoo Lu, Adilet Majit, Yernar Mukayev, Wen Rahme, Smarika Sharma, Sashank Silwal, Emaan Sohail, Yonathan Wagaye and Ahmed Walid.

Thank you also to Aisha Rahman and Manal Alhammadi for assistance with the admin work.

Content was inspired by and adapted from many sources, including:

• 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, also by Anders Mörtberg.
• The agda-unimath library by Elisabeth Stenholm, Jonathan Prieto-Cubides, Egbert Rijke, and many others.
• Introduction to Univalent Foundations of Mathematics with Agda by Martín Escardó.
• Introduction to Homotopy Type Theory by Egbert Rijke.
• [Lecture Notes for the course Logika v računalništvu 2021/22], by Danel Ahman and Andrej Bauer.

[Lecture Notes for the course Logika v računalništvu 2021/22]: https://www.andrej.com/zapiski/ISRM-LOGRAC-2022/00-introduction.html https://github.com/danelahman/lograc-2022

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 Haddock.