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.