Representation in Martin-Löf's type theory of subsets and other set-theoretical constructions used by working mathematicians. The idea is to add tools to deal with them and still preserve the intuitionistic and predicative nature of type theory.
Relevant papers on this topic are Building up a toolbox for Martin-Löf intuitionistic type theory: subset theory by G. Sambin and S. Valentini and The forget-restore principle: a paradigmatic example by S. Valentini.
Formalizing mathematics in Martin-Löf's type theory
Formalization of constructive mathematics, in particular of formal topology within Martin-Löf's type theory with the help of a proof-assistant.
For a development of universal algebra using some ideas of toolbox, see the PhD thesis by Venanzio Capretta.
Extensions of Martin-Löf's type theory
Investigation on the possibility of extending Martin-Löf's type theory with further constructors like powerset and quotients (see for example Can you add power-sets to Martin-Löf's intuitionistic set theory? by M. Maietti and S. Valentini and About effective quotients in constructive type theory by M.E. Maietti) still keeping as much as possible its constructive nature.
For related research on the connections between type theory and Aczel's constructive set theory, see the homepage of Nicola Gambino.
Normalization of type theories
New proofs of normalization for known lambda calculi like simple type theory, system F, intersection types (see for example A general method to prove the normalization theorem for first and second order typed lambda-calculi by V. Capretta and S. Valentini).
Investigation on the validity of canonical normal form theorems for extensional type theories, including internal languages of categorical universes (see for example An intuitionistic theory of types with assumptions of high-arity variables by A. Bossi and S. Valentini).
Connection between type theory and category theory
Development of internal type theories of categorical universes like topoi and pretopoi in the style of Martin-Löf's extensional type theory (see for example Modular correspondence between dependent type theories and categorical universes and "Joyal's arithmetic universes via type theory" by M.E. Maietti).
Other available papers about topics related to type theory can be found in the homepages of V. Capretta, N. Gambino, F. Guidi, M.E. Maietti, G. Sambin, S. Valentini.