[FOM] Re: Mirror versus opposite in categories

[Lengyel, Florian]

             McLarty writes: 

"[Lengyel] claims that the categorial idea of a dual can only be explained
by 
>an infinite egress of ever larger meta-categories." 

In fact, I made the somewhat weaker statement that the attempt to be more
explicit about the dualization functor * and the natural transformation op
"seems to" lead to an infinite egress, (in the sense that the simple
adjunction * -| * requires another level of metacategories to be expressed),
not that the notion "...of a dual can only be explained" that way.  Perhaps
I was mistaken to state there was any foundational trouble...

McLarty: 
"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" 

One goes by the conventions authors actually state; I haven't seen a
statement of the following one until now. 

McLarty: 
"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." 

Lengyel: 

One such purpose, for example, is to give the categorical reason why the
suggested typing convention--among others--is 'natural,'  once one is
explicit about the functor dual * and the natural isomorphism op. Given a
functor F:A->B, one has the naturality equation  F*(op_A(g)) = op_B(F(g)),
where g is a morphism of A. From this one derives four possible "natural"
conventions: explicitly notating (or suppressing) the functor dual *, and
explicitly notating (or suppressing) the natural transformation op. 

McLarty suggests suppressing both--this gives a correct reading of some
adjunction statements. It is on account of the naturality equation that this
particular type overloading is justified; the specific construction of B^op
is not as relevant, since "op" is a natural isomorphism..

Certain notions that could be kept separate--a functor and a natural
transformation--appeared to me to have been conflated in the literature, or
at least, indifferently notated. And I was concerned with a rather naïve
category theory; it might not be fair to compare it with ZF--set theorists
tend to be more meticulous. 

Another question: what is the state of the art in the foundations of
category theory? 

-Florian