small is beautiful

[Paul Taylor <pt10@PaulTaylor.EU>]

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