From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5873 Path: news.gmane.org!not-for-mail From: Colin McLarty Newsgroups: gmane.science.mathematics.categories Subject: Re: terminology Date: Thu, 27 May 2010 14:31:03 -0400 Message-ID: Reply-To: Colin McLarty NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1275151710 26648 80.91.229.12 (29 May 2010 16:48:30 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Sat, 29 May 2010 16:48:30 +0000 (UTC) To: categories@mta.ca Original-X-From: categories@mta.ca Sat May 29 18:48:28 2010 connect(): No such file or directory 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.69) (envelope-from ) id 1OIPD1-0006lJ-3E for gsmc-categories@m.gmane.org; Sat, 29 May 2010 18:48:27 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1OIObw-0005c2-PS for categories-list@mta.ca; Sat, 29 May 2010 13:10:08 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5873 Archived-At: Yes, Michael has said in several papers that his foundation would be given in FOLDS. And perhaps some specific version of the axioms has been given in some paper that I have missed. But I do not know of it; and when Martin-L=F6f suggested last year that I might want to pursue a type-theoretic foundation for category theory he did not mention knowing of one existing yet. So far as I know it remains a project. best, Colin 2010/5/26 John Baez : > Colin wrote: > > > As to articulating a way to avoid ever using identity of objects and >> identity of categories, John Baez writes >> >>> I think Michael Makkai has done it. =A0He has formulated a foundational >>> approach to mathematics based on infinity-categories, in which equality >>> plays no fundamental role: >>> >>> http://www.math.mcgill.ca/makkai/mltomcat04/mltomcat04.pdf >>> >>> I think some approach along these general lines might ultimately become >> quite popular. >> >> But so far as =A0know, this remains an approach, and not any specific se= t of >> axioms offered as foundation. >> > > > I should let Michael speak for himself, but I have the impression that he > intends to found all his work on FOLDS - "first-order logic with dependen= t > sorts". =A0In this paper: > > http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf > > he writes: > > "The restriction on the use of equality in FOLDS is a fundamental feature= . > FOLDS is to be used in formulating categorical situations in which, for > example, equality of objects of a category is not an admissible primitive= . > The absence of term-forming operators, to be interpreted as > functions, is a consequence of the absence of equality; it seems to me th= at > the notion of "function" is incoherent without equality. > > It is convenient to regard FOLDS a logic without equality entirely, and d= eal > with equality, as much as is needed of it, as extralogical primitives." > > Best, > jb > [For admin and other information see: http://www.mta.ca/~cat-dist/ ]