Good introductory book to type theory? 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.
 A: 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/ 
A: If your interest is type theoretic foundations, you might want to look into modern (type-theory based) theorem provers.  This is how I learned both type theory and dependent type theory.  This has the following advantages:


*

*Proof assistants let you "program in type theory".  This ability to manipulate type theoretic objects (and have a compiler yell at you when you do something wrong) was really helpful for me.

*Like Principia Mathematica, modern theorem provers are designed to be foundations of mathematics that can be used to formally prove theorems in mathematics.  And unlike ZFC (or even Principia), these systems are practically useable.  (Now, "practical" is relative.  They still are too cumbersome for a typical working mathematician, but they have nonetheless been used to formally prove a number of major theorems in mathematics.)

*The tutorials for these theorem provers are well-written, designed for a broad audience, and are not quite as intense as say the Homotopy Type Theory book.


There are some disadvantages to this approach.


*The tutorials I am about to list don't give much, if any, meta-theory on type theory.  While they will teach you how to prove things in type theory, they don't give proofs about type theory.

*Another disadvantage is that they might be a bit more geared to those who are CS literate.



I am biased since one of the authors is my advisor, but Theorem proving in Lean is a great way to learn dependent type theory and the Lean proof assistant.  It even has an online environment to try things out without having to install any software.
It is much older, but I also found the HOL-Light tutorial to be a good way to learn a weaker type-theoretic proof system.
A: I was going to write how I was surprised that nobody recommened Girard's book "Proofs and Types" yet, when I discovered that it actually had been disrecommended by someone.
Even though Girard tends to be a bit sloppy at times, he still manages to explain the core logical concepts much more lucently than for example "Programming in Martin-Löf's Type Theory".
It mainly does what the title suggests, namely explain the relation between proofs and types, i.e. the Curry–Howard correspondence. It also helps in familiarizing yourself with various bits of logic like the significance of cut-elimination. This should certainly be useful information if you're a mathematician trying to learn about the field.
P.S.: Here's also a list by Daniel Gratzer of various references on the subject.
A: Dan Grayson's paper An introduction to univalent foundations for mathematics is an exceptionally clear exposition.  The first half or so is a useful introduction to type theory generally, even if you're not interested in univalence.  The second half (on univalence) is even better.
A: Here are some resources:


*

*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ó.


*Univalent Foundations programme: Homotopy Type Theory: Univalent Foundations of Mathematics

*Bengt Nordström, Kent Petersson, and Jan M. Smith: Programming in Martin-Löf's Type Theory
A: I am far from being an expert. I will make a few suggestions.

*

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


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


*Andre Joyal. Notes on Clans and Tribes.


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


*Thorsten Altenkirch. Naïve Type Theory.
A: This entry level overview of pure type systems might be helpful: http://www.rbjones.com/rbjpub/logic/cl/tlc004.htm
Roorda's masters' thesis http://www.staff.science.uu.nl/~jeuri101/MSc/jwroorda/thesis.ps goes into PTS further, though from a programming language theory perspective.  
I've been wanting to read Barendregt's Lambda Calculus with Types: ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps
This paper by Martin-Löf is pretty readable: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.131.926&rep=rep1&type=pdf
Also some lecture notes: http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf
There is a ton of stuff on ncatlab.org.
A: As in Jason's answer, I recommend starting with an implementation like agda.
I like the presentation in Diviánszky Péter - Agda tutorial
and Wadler, Wen Kokke, and Siek - Programming Language Foundations in Agda.
