I don't know anything about type theory and I would like to learn it.
I'm interested to know how we can found mathematics on it.
So, I would be interested by any text about type theory whose angle is similar to the one of Russel and Whitehead in the Principia, or similar to the one of Bourbaki (for instance).
But, I am also interested by any nice presentation of type theory (without any special focus on foundation of mathematics) that would help me to get the best of it.
Books, texts, articles, links are welcomed.
I am interested by any type theory (Martin-Löf's, homotopic, etc.).
PS:
If it can help, in a way, by "foundation of mathematics", I mean "total formalization of mathematics", as in Bourbaki for instance.
PPS:
I have asked another related question there, a little bit more general.
Best Answer
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/