Good introductory book to type theory?

Here are some resources:

  1. UniMath school teaching materials, and in particular:

    • Spartan type theory, an introduction to type theory (slides)

    • Introduction to Univalent Foundations of Mathematics with Agda by Martín Escardó.

  2. Univalent Foundations programme: Homotopy Type Theory: Univalent Foundations of Mathematics

  3. Bengt Nordström, Kent Petersson, and Jan M. Smith: Programming in Martin-Löf's Type Theory

I am far from being an expert. I will make a few suggestions.

  1. Per Martin-Löf. Intuitionistic type theory. (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli, Bibliopolis, 1984

  2. T. Streicher (1991), Semantics of Type Theory: Correctness, Completeness, and Independence Results, Birkhäuser Boston.

  3. Andre Joyal. Notes on Clans and Tribes.

  4. Michael Shulman. Homotopy type theory: the logic of space.

  5. Thorsten Altenkirch. Naive Type Theory.


It seems that the HoTT book and Vladimir Voevodsky’s program for Univalent Foundations of Mathematics is made for you !

You will find everything from here: https://homotopytypetheory.org/