Almost two decades ago I studied Type Theory in Uruguay on a course organized, if I remember correctly, by Gustavo Betarte and Alvaro Tasistro. In those times we used "Programming in Martin Lof type theory" by Nordstrom. I don't know if this is still considered to be the best introduction. In any case, anyone interested in Type Theory may also be interested in a 2000 document made recently available by Bob Walters in http://rfcwalters.blogspot.com.ar/2013/10/interview-with-bill-lawvere-by-fel... It contains historical information that I am pretty sure is not available in other sources and that should help any newcomer to understand Type Theory in a broader categorical context. Mat?as Menni. "Vasili I. Galchin" <vigalchin@gmail.com> escribi?:
Hello Cat List,
I have downloaded many papers about Martin-Lof type theory papers ( .... maybe I just need to pound my head against the wall like other areas that I have I learned until a light goes on my mind?). However, any help on gentle tutorials on this subject would be much appreciated.
Kind regards,
Vasili
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]