From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5496 Path: news.gmane.org!not-for-mail From: Paul Taylor Newsgroups: gmane.science.mathematics.categories Subject: small is beautiful Date: Fri, 8 Jan 2010 14:33:07 +0000 Message-ID: Reply-To: Paul Taylor NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 (Apple Message framework v624) Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1263048212 9531 80.91.229.12 (9 Jan 2010 14:43:32 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sat, 9 Jan 2010 14:43:32 +0000 (UTC) To: categories list Original-X-From: categories@mta.ca Sat Jan 09 15:43:21 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 1NTcX9-0005lE-1z for gsmc-categories@m.gmane.org; Sat, 09 Jan 2010 15:43:19 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1NTc4l-0003dx-55 for categories-list@mta.ca; Sat, 09 Jan 2010 10:13:59 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5496 Archived-At: I largely agree with Bob Pare's New Year's Day posting, and disagree with those who disagree with him, although Albert Burroni is right to generalise from categories to structures. > ... there were two kinds of categories in practice. [Large and small.] > I went on to say that there were then four kinds of functors. > - Functors between large categories were to be thought of as constructions > of one structure from another, e.g. the group ring. > - Functors between small categories were interpretations of > one theory in another or reindexing or rearranging. > - Functors from small to large categories were models or diagrams > in the large one. These kinds of functors are perhaps the most important > of the four, although this may be debatable. > - The fourth kind, from large to small are rarer. They can be thought > of as gradings or partitions of the large category. > Small categories -> equality of objects okay > Large categories -> equality of objects not okay > Small is beautiful, not evil. I would, however, like to substitute INTERNAL for SMALL. Tradionally, a "small" category is one with a "set" of objects and morphisms. However, since set theory is the problem and not the solution to the foundations of mathematics, we can avoid this by translating "set" into "object of a topos" and more generally a lex category (one with pullbacks and a terminal object") or an arithmetic universe. (I believe that there was a development of "locally internal" instead of "locally small" categories by some French categorists in the 1970s -- Burroni again maybe?.) Having done this, I would like to rescue the word "set" from the set theorists, and use it to mean "object of a topos", lex category or arithmetic universe. Vaughan Pratt's remark that "FinSet is an essentially small category" is entirely consistent with what Bob said. FinSet is a LARGE category for which there is a SMALL category "finset" (whose set of objects is N) and a WEAK EQUIVALENCE, ie a full and faithful functor finset->FinSet that is essentially surjective. This is one of the "most important" functors, according to Bob. An internal category (and more generally internal structure) of course inherits equality from its carrier, which is by definition a set (object of a topos or lex category). A large category or external structure has no carrier, and therefore no notion of equality, as Bob said. Another way of seeing the large/small or external/internal distinction is that a small or internal structure gives a NAME to the external one, which we may conversely call the SEMANTICS (meaning) of the name. So, again, I agree with Bob in identifing semantics/syntax with large/small. You might object that this is a syntax without an alphabet of symbols. Again we need an internal notion, this time an INTERNAL LANGUAGE. Unfortunately, a lot of people have muddled up the terminology here. What *I* mean by an internal language is an internal structure of a suitable kind for investigating formal grammar. For example, its set of "words" is the internal free monoid on its set of "letters", which is why we need an arithmetic universe. Regrettably, other people have used the phrase "internal language" to mean a language that is equivalent to a structure, which I call a PROPER LANGUAGE, where I have anglicised French "propre" or Italian "proprio". Given, for example, an internal CCC, it has a proper language that is an INTERNAL SIMPLY TYPED LAMBDA CALCULUS. From this we may construct the internal CATEGORY OF CONTEXTS AND SUBSTITUTIONS, which is the internal CLASSIFYING CATEGORY for the lambda calculus, in particular having an internal stucture-preserving functor to the given internal CCC, and this is an interval equivalence. (I'm not going to go into whether it is a weak or a strong equivalence -- see Section 7.6 of "Practical Foundations" for this.) Besides the book, please see also mathoverflow.net/questions/8731/categorical-foundations-without-set- theory Paul Taylor [For admin and other information see: http://www.mta.ca/~cat-dist/ ]