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/ ]