Type theory as foundations

Does anyone know any good references that describe type theoretical foundations of mathematics? I've read some books e.g. Winskel's The Formal Semantics of Programming Languages and Pierce's Types and Programming Languages. However, these don't address foundational issues, since they are geared towards practical programming language semantics and don't assume any knowledge of logic.

What troubles me is that almost any definition of mathematics has a set as part of the definition, so any foundation would somehow have to address sets and elements that we use in order to concretely compute (unless I'm completely missing the point). Is there any rigorous book that starts by giving a precise definition of what a type is and how it can be used to describe foundations? Every book I've read so far has failed to even give a precise definition of a type.

As much as I can confirm that (the introduction and the type theory chapter of) the homotopy type theory book is well written, I have the impression that there are shorter texts focusing more directly on (the history of) type theory as foundations. The Stanford Encyclopedia of Philosophy (SEP) is an excellent place where one can find such shorter texts. A good place to start might be the section on typed theories in Randall Holmes' SEP entry on Alternative Axiomatic Set Theories. A more complete picture including $\lambda$-calculus can be found in Thierry Coquand's SEP entry on Type Theory. The latest revision of that entry even contains a section on univalent foundations (homotopy type theory).

I have to admit that the SEP articles are quite broad and contain many historical and philosophical references. For some more mathematically minded people, a more focused account like William Farmer's The Seven Virtues of Simple Type Theory might be better suited as an introduction to type theories (as foundation). One problem with type theory as a foundation is that there are so many different (non-equiconsistent) type theories. For set theory, this problem can be avoided by using ZF (or NBG) as the "canonical" set theory. Saunders Mac Lane (1986) tried to address this problem by advocating "bounded Zermelo set theory" as a foundation for mathematics:

Some weaker subsystems of ZFC are used. Zermelo set theory, the system Z described above, is still studied. The further restriction of the axiom of separation to formulas in which all quantifiers are bounded in sets ($\Delta_0$ separation) yields "bounded Zermelo set theory" or "Mac Lane set theory", so called because it has been advocated as a foundation for mathematics by Saunders Mac Lane (1986). It is interesting to observe that Mac Lane set theory is precisely equivalent in consistency strength and expressive power to TST with the Axiom of Infinity. Z is strictly stronger than Mac Lane set theory; the former theory proves the consistency of the latter. See Mathias (2001) for an extensive discussion.

In an answer to another question, I tried to explain how TST is related to other type theories, and how it derives its consistency strength from non-circular impredicative quantification.