What is needed before a trace can be written

The hypothesis ladder is strict.

• Rigidity is what types ${\mathrm{Tr}}_L(a)$ and ${\mathrm{Tr}}_R(b)$ at all, because their formulas use evaluation and coevaluation maps.
• A chosen comparison $j_X:X\to X^{\vee \vee }$ turns an endomorphism $x:X\to X$ into a traceable morphism $j_{X}x$. A pivotal structure supplies such comparisons as monoidal isomorphisms.
• Sphericality is an additional condition guaranteeing that the left and right traces agree.
• In a braided rigid category, the Drinfeld morphism $u_X:X\to X^{\vee \vee }$ from A braided rigid category has a Drinfeld morphism already makes ${\mathrm{Tr}}_L(u_{X}x)$ well typed. This Drinfeld morphism is already a natural isomorphism under the bare braided-rigid hypotheses, but it need not be monoidal; a twist is what combines with it to produce a pivotal structure.