Carlo Angiuli • Daniel GratzerPrinciples of dependent type theoryhttps://www.danielgratzer.com/courses/type-theory-s-2024/lecture-notes.pdf