19 Jan
2010
19 Jan
'10
4:48 a.m.
[[sorry about the delay with replying: i am travelling.]] On Jan 14, 2010, at 6:23 AM, Colin McLarty wrote:
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?
i am not aware of any of martin-loef's writings on the web. i was talking from memory (as i am not near my filing cabinet with the paper copies). martin-loef's category theory example could be in his bibliopolis book, or in one of his Logic Colloquium contributions. -- dusko [For admin and other information see: http://www.mta.ca/~cat-dist/ ]