These are the student written lecture notes for the course being taught by Professor Robert Harper on Computational (Higher Dimensional) Type Theory.
To build the lecture notes, simply run make
. This requires the
presence of latexmk
on the
system.