For rigid symmetric monoidal categories, there is in fact always a duality functor, unique up to isomorphism (without symmetry you would have to specify what you mean by "dual").

Here is a possible proof of existence:

Consider the following category $\tilde C$, its objects are quadruples $(x,y,\eta,\epsilon)$ where $x,y$ are objects of $C$ and $\eta: 1_C\to x\otimes y$ is a morphism in $C$, and $\epsilon : y\otimes x\to 1_C$ is another morphism, together exhibiting $y$ as a dual of $x$.

A morphism $(x_0,y_0,\eta_0,\epsilon_0)\to (x_1,y_1,\eta_1,\epsilon_1)$ is a pair of morphisms, $f :x_0\to x_1, g : y_1\to y_0$ such that $g$ "is dual to $f$" in the following sense: the composite $$y_1\cong y_1\otimes 1_C \to y_1\otimes x_0\otimes y_0\to y_1\otimes x_1\otimes y_0 \to 1_C\otimes y_0\cong y_0$$
is equal to $g$, where I've used the unitors of $C$, the map $\eta_0$, then $f$, and $\epsilon_1$ .

Composition is the obvious one, where you have to check that the "dual" of $f\circ f'$ is the dual of $f'\circ$ the dual of $f$. This check is essentially going to come up in any proof, and is the essential part of the proof - you should try to do that check.

I then claim the following two things: the forgetful functor $\tilde C\to C, (x,y,\eta,\epsilon)\mapsto x$ and $(f,g)\mapsto f$ is an equivalence of categories.

The fact that it is essentially surjective comes from the fact that $ C$ is rigid, and fully faithfulness comes from the fact that for any $f$ there is a unique $g$ which works (namely, the composite that I described !).

Then you get the following zigzag $C\overset\sim\leftarrow \tilde C\to C^{op}$ where the second arrow is projection to $y$ (and $g$)

Now, equivalences have quasi-inverses (if you have the axiom of choice, or a canonical choice of a dual and duality data for any $x$ - which you don't need to be functorial *a priori*), so that gives you a well defined functor $D: C\to C^{op}$ which is obviously an equivalence.

Unicity (up to natural isomorphism) is not hard to prove, you should try that !

It gets a little bit more complicated for higher categories. A functor $D$ is always definable, in a similar way as above (although the definition of $\tilde C$ needs to be changed a bit, because you need to specify a $2$-morphism witnessing one of the triangle identities), but saying what it does on objects and morphisms is no longer enough to fully determine it as a functor - the obstruction is exactly the same obstruction as the unicity of a functor which is the identity on objects and on $1$-morphisms.

4more comments