[FOM] Opposites, again.

[Lengyel, Florian]

>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...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. 
> 

Some remarks: 

To pursue the analogy with ZF, one might trade meta-categories for theorem
schema about meta-categories. In the absence of classes or universes, if one
were to interpret category theory within ZF, one possibility is to treat the
object class of a large category in the same manner as one treats a proper
class such as ON, the class of ordinals: classes are formally
indistinguishable from formulas of the language of ZF. A true statement
about all classes in ZF amounts to a theorem schemata: transfinite induction
on ON is an example. 

In a theory of (a category of all) categories, one could still work with
meta-categories or a category of all categories in the guise of
abbreviations for certain formula referring to all categories; true
statements about all categories in the language of the theory would amount
to theorem schemata. 

As for typing, I should give a definition (to attempt to avoid trouble): the
type of a morphism f of a category C is given by the pair (dom(f),cod(f)),
where dom and cod are the domain and codomain maps of C, as usual. I was
under the impression this is the standard typing of morphisms (I don't take
credit for it). So, I do not rule out the possibility that f = f^op in the
opposite category C^op. 

>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.
>This typing convention relies on the fact that the objects and arrows 
>of B^op are by definition the objects and arrows of B. 

Ok. The usual typing convention leads to the same kind of overloading, based
on naturality equations; these handle type identifications (e.g.,
identifying F with F*). Taking a foundational attitude, it is fair to
mention one or the other convention, if one is going to overload operators.

For me, the universal property of the opposite category takes care of naming
and typing at once:  given a category A, an opposite category to A is a pair
<op_A, A^op>, where A^op is a category and op_A: A -> A^op is a
contravariant functor such that for every category B and for every
contravariant functor F: A->B, there is exactly one covariant functor
F*:A^op -> B such that   F* op_A = F.  If F:A->B is a (covariant) functor,
form the composite op_B o F :A ->B^op. By the universal property, there is a
unique covariant functor   F*:A^op -> B^op with op_B F = F* op_A   (a reason
not to conflate op and *, if it matters). 

The assertion that " The opposite functor A -> A^op is a natural
transformation from the identity functor (on the meta-category of
categories) to the functor dual *" would be an abbreviation for a theorem
schemata in a theory of categories in which "op" and "*" are operators (they
can be overloaded as "op", but I err on the side of distinguishing between
F*:A^op->B^op and F^op:B->A--just in case not every category is a coproduct
of monoids). If one does without meta-categories, one could still
have something like them with theorem schemata. 

Another minor point concerning the opposite: some authors set f^op = f,
switch the domain and codomain, and reverse the order of composition. Mac
Lane does not insist that the arrows of C^op are identical; he writes, "the
objects of C^op are the objects of C, the arrows of C^op are arrows f^op, in
one-one correspondence f |-> f^op with the arrows f of C." One wants the
universal property; one hesitates to take f^op=f too literally, in view of
the

Example: the converse relation of a preorder (X, <=) is customarily defined
by transposing the ordered pairs of the relation <=. If one insists that the
opposite (X, <=)^op of this preorder as a category must have the same arrows
(i.e., ordered pairs) as (X, <=), then for this model of the opposite the
ordered pairs are the same, but the projections of the product XxX
(restricted to <=) are interchanged. This creates two notions of a converse,
different for inessential reasons. The universal characterization of the
opposite category above allows for either case, and it comports with the
typing I've indicated (or either typing).