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.

primitivenotions. You can get used to these notions, and analogies with your pre-existing mathematical knowledge can be made, but there can be no precise explanation. $\endgroup$ – Andrej Bauer May 6 at 22:08