[FOM] Re: Mirror versus opposite in categories

[Colin McLarty]

I am glad to see Florian Lengyel apply such vigorous thought to the 
presentation of category theory, and perhaps he has the right idea for 
strictly typed presentations.  His main points, though, seem to me to rest 
on specific conventions which are not the only ones possible.

He claims that the categorial idea of a dual can only be explained by

>an infinite egress of ever larger
>meta-categories.

This is true for one pattern of explanation: that is if you take 
dualization as a functor defined on a meta-category of categories (taking 
each one of them to its dual), and so as an arrow in the next higher 
meta-category. Since the next higher also has duals, we need a functor 
defined on it, and so on.

To my mind, that is a good pattern of explanation, and we should feel free 
to posit those meta-categories as far as we like.  But it is not the only 
possible pattern.  The weakest one would merely take dualization as a 
operator on the category of categories, and not a functor, and thus would 
take not one step to any higher meta-cat.  Of course we would all know this 
operator is functorial, just like we all know there is a class of all 
ordinals, but our theory could refuse to formalize that, just as ZF refuses 
to name proper classes.


Also Florian Lengyel believes there is a type error in several books on 
category theory.  He writes:

>given functors F:A->B and U:B->A,
>F -| U (F is left-adjoint to U) if there is a natural isomorphism
>B(F(-),-) ->A(-,U(-)).
>
>This has a type error: the domain of B(-,-) is B^op x B, but F has codomain
>B,  not B^op

But the books are strictly correct on one natural convention:  We say each 
term (name of an object or arrow) has a category as type, and when a term 
of type B occurs as the first argument in a hom term it is construed as 
having type B^op.  So the term F(-) has type B and when it occurs in 
B(F(-),-) it is construed as having type B^op.  This is just like any 
computer language that construes integer terms as real terms when they 
occur in arithmetic expressions along with real terms.

This typing convention relies on the fact that the objects and arrows of 
B^op are by definition the objects and arrows of B.  So there is no 
ambiguity about the referent of a term---just as there is no ambiguity 
about how to construe an integer as a real number.

Yet Florian Lengyel's way of typing has advantages for some purposes.

best, Colin