From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5527 Path: news.gmane.org!not-for-mail From: Colin McLarty Newsgroups: gmane.science.mathematics.categories Subject: Re: equality Date: Thu, 14 Jan 2010 09:23:29 -0500 Message-ID: References: Reply-To: Colin McLarty NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 X-Trace: ger.gmane.org 1263524992 28388 80.91.229.12 (15 Jan 2010 03:09:52 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 15 Jan 2010 03:09:52 +0000 (UTC) To: Categories Original-X-From: categories@mta.ca Fri Jan 15 04:09:45 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1NVcZC-00016U-W3 for gsmc-categories@m.gmane.org; Fri, 15 Jan 2010 04:09:43 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1NVbyH-0007WE-KJ for categories-list@mta.ca; Thu, 14 Jan 2010 22:31:33 -0400 In-Reply-To: Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5527 Archived-At: 2010/1/13 Dusko Pavlovic : > 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/ ]