From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6250 Path: news.gmane.org!not-for-mail From: Michael Shulman Newsgroups: gmane.science.mathematics.categories Subject: Re: Not invariant but good Date: Tue, 28 Sep 2010 16:11:06 -0700 Message-ID: References: Reply-To: Michael Shulman 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 1285802089 7812 80.91.229.12 (29 Sep 2010 23:14:49 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Wed, 29 Sep 2010 23:14:49 +0000 (UTC) Cc: categories To: John Baez Original-X-From: majordomo@mlist.mta.ca Thu Sep 30 01:14:47 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.138]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1P15rK-0003b6-PB for gsmc-categories@m.gmane.org; Thu, 30 Sep 2010 01:14:46 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:40484) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1P15qY-0000UO-QN; Wed, 29 Sep 2010 20:13:58 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1P15qV-0001UJ-Rm for categories-list@mlist.mta.ca; Wed, 29 Sep 2010 20:13:56 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6250 Archived-At: On Sun, Sep 26, 2010 at 10:36 PM, John Baez wrote: > Can every property of categories that is invariant under equivalence be > expressed in some language that doesn't include equations between objects= ? > Or conversely? Or what precise conditions are needed to get theorems alon= g > these lines? The converse is very easy, and it's something that I and others have frequently mentioned in these discussions: if we write category theory in dependent type theory with arrows dependent on their source and target and no equality predicate on objects, then all formulas and constructions in this language are easily proven to be invariant under equivalence and isomorphism. The forward direction is trickier, but essentially the answer is yes: I believe theorems along these lines can be found in: 1) Peter Freyd, "Properties invariant within equivalence types of categories", 1976 2) Georges Blanc, "=C9quivalence naturelle et formules logiques en th=E9orie des cat=E9gories", 1979 3) Michael Makkai, "First-order logic with dependent sorts, with applications to category theory," http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf (and perhaps others that I'm unaware of). Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ]