Home

Awesome

Introduction to univalent foundations of mathematics with Agda

There is a modular version of the Agda files here at https://github.com/martinescardo/TypeTopology in the folder source/MGS/.

Sources to generate the lecture notes available at

https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html

https://arxiv.org/abs/1911.00580

Agda 2.6.2.1 or higher is required. Consult the installation instructions to help you set up Agda and Emacs for the Midlands Graduate School.