I think the first recommendation would be the SEP (Stanford Encyclopedia of Philosophy) article on Type Theory written by Couquand [1]. It is a broad but well f

I think the first recommendation would be the SEP (Stanford Encyclopedia of Philosophy) article on Type Theory written by Couquand [1]. It is a broad but well founded walk through the basis of type theory and it’s usage as a foundation for both logic and mathematics. It also contains a section discussing Univalent Foundations, which is the foremost area for type theoretic foundations at present. The papers listed in the reference section contain most of the fundamental research results of note. I do think Aczel’s “The type theoretic interpretation of constructive set theory” (1978) and Bell’s “Types, Sets and Categories” (2012), which are both cited are good papers. 1 —- https://plato.stanford.edu/entries/type-theory/ https://plato.stanford.edu/entries/type-theory/