This is a list of type theory resources: https://github.com/jozefg/learn-tt https://github.com/jozefg/learn-tt This is an exposition of Martin-Lof's dependent

This is a list of type theory resources: https://github.com/jozefg/learn-tt https://github.com/jozefg/learn-tt This is an exposition of Martin-Lof's dependent type theory: http://www.cs.nott.ac.uk/~psztxa/mgs-17/notes-mgs17.pdf http://www.cs.nott.ac.uk/~psztxa/mgs-17/notes-mgs17.pdf Section 5 is about Homotopy Type Theory (HoTT), a newer type theory that is still being developed. Chapter 1 of the HoTT book introduces Martin-Lof's dependent type theory, then the rest of the book covers HoTT-specific topics: https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/