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](https://mathoverflow.net/q/330922/115872), a little bit more general.



Good introductory book to 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/> 


