Introduction to HoTT/UF with Agda

Basic course for MGS 2022

Martin Escardo (University of Birmingham)

We introduce Homotopy Type Theory and Voevodsky's Univalent Foundations using Agda.

Lecture Notes.


Last modified: Mon Feb 14 16:26:23 GMT 2022