From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5845 Path: news.gmane.org!not-for-mail From: "Paul Taylor" Newsgroups: gmane.science.mathematics.categories Subject: equivalence terminology Date: Mon, 24 May 2010 14:42:21 +0100 Message-ID: References: Reply-To: "Paul Taylor" 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 1274808631 2000 80.91.229.12 (25 May 2010 17:30:31 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Tue, 25 May 2010 17:30:31 +0000 (UTC) Cc: "Colin McLarty" To: categories@mta.ca Original-X-From: categories@mta.ca Tue May 25 19:30: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 1OGxxU-0006MW-7B for gsmc-categories@m.gmane.org; Tue, 25 May 2010 19:30:28 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1OGxHX-000145-QS for categories-list@mta.ca; Tue, 25 May 2010 13:47:07 -0300 In-Reply-To: Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5845 Archived-At: Colin McLarty said, > It is an interesting impulse in higher category theory to avoid > identity in favor of isomorphism on the level of objects, and to avoid > isomorphism in favor of equivalence on the level of categories. But > so far as I know no one has yet articulated a way to avoid ever using > identity of objects and identity of categories. I am not going to get involved in higher category theory, but one setting in which (essentially) the question of identity of objects arises is in the interpretation of type theories in categories, where one needs to "choose" binary products, to give the simplest case. Any type theory has its category of contexts and substitutions (or classifying category). This has the categorical structure that is analogous to the type theoretic connectives, for example it's a CCC if we started with lambda calculus. Conversely, any category has its proper language, consisting of names for its objects and morphisms and various axioms. Without even having the structure, let alone a choice of it, the category is embedded in the category of contexts and substitutions of its proper language. If the category has choices for the structure then this embedding is a strong equivalence, ie with a pseudo-inverse, If it has the structure but not choices for it then it is a weak embedding - full, faithful and essentially surjective. The upshot of this is that, by replacing the category with a weakly equivalent one, you become able to talk about equality of objects, choices of product, etc. In other words, using the principle of interchangeability at a higher categorical level, we get the convenience of working with equality in the original structure. This is all explored in my book, "Practical Foundations of Mathematics". Paul [For admin and other information see: http://www.mta.ca/~cat-dist/ ]