From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5861 Path: news.gmane.org!not-for-mail From: John Baez Newsgroups: gmane.science.mathematics.categories Subject: Re: terminology Date: Wed, 26 May 2010 09:28:50 +0100 Message-ID: References: Reply-To: John Baez NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 X-Trace: dough.gmane.org 1274968140 32250 80.91.229.12 (27 May 2010 13:49:00 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 27 May 2010 13:49:00 +0000 (UTC) Cc: categories@mta.ca Original-X-From: categories@mta.ca Thu May 27 15:48:59 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 1OHdSD-0002k2-7z for gsmc-categories@m.gmane.org; Thu, 27 May 2010 15:48:57 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1OHdB9-00063m-LV for categories-list@mta.ca; Thu, 27 May 2010 10:31:19 -0300 In-Reply-To: Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5861 Archived-At: 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. He 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 know, this remains an approach, and not any specific set 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 dependent sorts". In 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 that the notion of "function" is incoherent without equality. It is convenient to regard FOLDS a logic without equality entirely, and deal 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/ ]