Type theory lectures

This repo hosts the slides I have made to accompany my intermittent lectures on dependent type theory.

I am not a professor or anyone qualified to teach type theory; these lectures are entirely a learning tool for myself to better understand the theory (by teaching it to my mildly-interested friends). For more correct and thorough reading material on type theory, please refer to the books I've based my lectures on:

• The lecture notes of Carlo Angiuli and Daniel Gratzer's course on Modern Dependent Type Theory.
• The Homotopy Type Theory book: HoTT

Compiling

Compile the slides to PDF using typst:

typst c lecture_1_slides.typ

PDFs

Or, if you don't want to compile, look at the releases:

• Lecture 1 PDF