Re: equality

2010/1/13 Dusko Pavlovic <dusko@kestrel.edu>:

hi.

several people suggest dependent type theory as a foundation to formalize categories. maybe it is worth mentioning that per martin- loef (the originatory of dependent types) worked this out, prolly in the 70s.

Is there a published account of this, preferably on the web? Colin [For admin and other information see: http://www.mta.ca/~cat-dist/ ]