Is there any comprehensive definition of the opposite category $\mathcal C^{op}$ of a category $\mathcal C$?

Question

In the definition of the opposite category $\mathcal C^{op}$ of a category $\mathcal C$, it is said that : objects remain the same and arrows' directions are changed (that is, and arrow $f:A \to B$ in $\mathcal C$ is and arrow $f:B \to A$ in $\mathcal C^{op}$, and vice versa. Now I think this can not be a safe definition in general. Here goes the story:

Consider the definition of a product and coproduct of two objects $A$ and $B$ in a category $\mathcal C$. If we convert the diagram of a product in its "dual form" in the opposite category $\mathcal C^{op}$ (that is, by definition of $\mathcal C^{op}$, letting the objects remain the same and convert the arrows' directions) we gain a diagram similar to the diagram of a coproduct in $\mathcal C$ (defined directly in $C$). I bold "similar" since they can not be equal! In fact, if they were equal, we would have $A+B=A\times B$ and we know by certain that they are not. (E.g., consider a poset $P$ and we know that $x \times y=g.l.b(x,y)$ and $x + y=l.u.b(x,y)$ and those are not the same).

In short, one can not gain a coproduct in $\mathcal C$ simply by re-writing a product in $C$ in its dual form in $\mathcal C^{op}$. Preservance of objects makes troubles.

Now given this, don't you think we must have a more comprehensive definition of $\mathcal C^{op}$, for example one that converts the objects to their duals (defined directly and independently from the traditional $\mathcal C^{op}$ , not themselves (which will work for single objects too: their dual is the same as the original)?

$**$ You can see the attached image from Awodey's text, in order to see the products/coproducts and their related diagrams:

Answer 1

Nobody claims that $A \times B = A + B$ holds in $\mathcal{C}$. But it is true that $A \times^{\mathcal{C}} B = A +^{\mathcal{C}^{op}} B$, where the supscript denotes the category in which we take the (co)product. More generally, $\lim^{\mathcal{C}}=\mathrm{colim}^{\mathcal{C}^{op}}$. If you want to rename your objects in the dual category - that's ok. In this case, we have $(A \times^{\mathcal{C}} B)^{op} = A^{op} +^{\mathcal{C}^{op}} B^{op}$, which may be even abbreviated to $(A \times B)^{op} = A^{op} + B^{op}$.

Answer 2

There's no problem. The exact definition of $\mathcal{C}^{op}$ is as a quintuple $(\text{ob}\mathcal{C},\text{mor}(\mathcal{C}),t,s,\circ^{op})$ where $\circ^{op}(f,g)=\circ(g,f)$. That is, $\mathcal{C}^{op}$ has the same objects and morphisms, the source and target functions of $\mathcal{C}$ serve as the target and source functions, respectively, of $\mathcal{C}^{op}$, and the composition function is replaced with its reverse. This definition satisfies associativity and the existence of units, and thus gives another category structure on the objects and morphisms of $\mathcal{C}$. Then a product diagram in $\mathcal{C}$ is exactly the same thing as a coproduct diagram in $\mathcal{C}^{op}$.

If it makes you more comfortable, it's certainly possible to introduce symbols $X^{op},f^{op}$ for each object $X$ and morphism $f$ of $\mathcal{C}$, and put a category structure on these to define $\mathcal{C}^{op}$. Such a structure will be isomorphic.

But there's no need to do this, and Awodey's definition is certainly comprehensive.