@YemonChoi True. But note that you can define trace for an endomorphism of a dualizable object even if the category doesn't have duals for all objects.

There's only one morphism $I\to I$ so the trace would be trivial even if it was defined.

@geodude The étalification comonad is idempotent. I don't know what you mean by "universal covering" in this context.

Saying there are "at least as many" is false in some sense. Different adjuctions $(G,F)$ can give the same comonad $F\circ G$.

@FrançoisG.Dorais Why does this only work for effectively axiomatizable theories?

@ZhenLin Could you point out where the following argument falls down? Claim: If $A$ and $B$ are well-orderable then so is $A^B$. Proof: Let $\alpha\simeq A$ and $\beta\simeq B$ be ordinals. Then $\alpha^\beta$ is hereditary-ordinal-definable. Since Choice holds in HOD, $\alpha^\beta$ is well-orderable. Then since $A^B\simeq\alpha^\beta$ we have that $A^B$ is well-orderable.

I'd argue that categories really should be named after their objects, but that you can only tell what the objects really are by looking at the structure of the morphisms. For example the category $\mathbf{Rel}$ of "sets" and relations should really be called $\mathbf{FreeSupLat}$.

There's a nice paper "Morphism Axioms"(pdf) by Florian Rabe that suggests that one should specify additional axioms for a first order theory that say what the morphisms between models should be. This means that you don't have to worry about equivalent theories having inequivalent categories of models, because you can just explicitly define the morphisms.

@Gro-Tsen It's hard to contact people via mathoverflow, so I sent him an email.

"In a category with internal homs $[-,-]$, given an object $S$, the continuation monad is the endofunctor $X\mapsto[[X,S],S]$." ncatlab.org/nlab/show/continuation+monad

By the way, I think your nice properties only hold when the tensor has an even number of indices (i.e. $m$ is even). For example when $m=1$ your formula reduces to saying that $\mathrm{Det} v$ is just the product of the entries of $v$, which is clearly not basis-independent even if we restrict the possible change-of-basis matrices to unitaries with determinant $1$.