categories: Re: Time for functors to grow up; three queries

["Jonathan Kirby" <jkirby@maths.man.ac.uk>]

From: "Dr. P.T. Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
>
> This is really a consequence of the fact that you're thinking of the
> category of sets as a unique entity (if not God-given, then at least
> handed down to us by Zermelo and Fraenkel). Of course, if you have two
> equivalent single-sorted theories, and you consider their models in the
> same category, you will get isomorphic categories of models. But that
> won't happen if you consider equivalent theories whose underlying sorts
> are different; nor will it happen if you consider models of the same
> theory in two equivalent categories (for example, the category of sheaves
> on a space X and the category of local homeomorphisms over X -- even for
> a one-point space X, these aren't isomorphic, though they are both
> equivalent to (Sets)).

Some terminology I find useful for this concept I have borrowed from Wilfred
Hodges' book "Model Theory". He defines two theories A and B (within some
fixed system) in formal languages L1 and L2 to be "definitionally
equivalent" if there is a third theory C in a language L3 extending both L1
and L2 such that the forgetful functors between the categories of models
Mod(C) -> Mod(A) and Mod(C) -> Mod(B) are both isomorphisms, and there is a
given way of calculating their inverses. (This is not exactly how he defines
it, since he doesn't use the concept of categories.)

The definition can obviously be generalized from this model theory context.
In this language, Peter Johnstone's remark can be rephrased as saying that
definitional equivalences between theories in the same underlying structure
(category) are always isomorphisms of categories, but definitional
equivalences between theories in different underlying structures are
generally only equivalences. (But the categories of models of one theory in
different categories may not be equivalent at all, for example the
categories of groups in Set and in the category of finite sets.)

Perhaps the terminology "definitional isomorphism" would also be useful,
where appropriate.

Jonathan