I just found a 2007 PhD thesis on topics surrounding intuitionistic type type theory that has blown me away.
Warning: many of the regulars on MO are likely to find this work way too philosophical for their tastes (as per their many comments on MO). They should also note that his copious references heavily favour slightly older mathematics, but by mathematicians of high stature. In other words, as I have said here before, it really seems like "mathematical taste" has shifted far away from the more philosophical stance that some of the Giants of mathematics used routinely.
