I'm not completely clear on what answer would be considered satisfactory, but here's one categorical way to think about tracing in $\mathbf{Bij}$.

The morphisms of the symmetric monoidal category with duals obtained by applying the Joyal-Street-Verity construction to $\mathbf{Bij}$ can be pictured in terms of string diagrams that are essentially 1-cobordisms, i.e, curves bounded by compact 0-manifolds that are built from string diagrams for permutations and from cups and caps (which are counits and units of dual pairs) by applying the usual composition and juxtaposition operations. Now cobordisms generally are certain types of cospans in the category of manifolds. Thus, what we can do is consider $\mathbf{Bij}$ (or more generally $\mathbf{Set}$) as embedded in the bicategory of cospans between sets, where a bijection or function $\sigma: A \to B$ is mapped to the cospan

$$A \stackrel{\sigma}{\to} B \stackrel{1_B}{\leftarrow} B.$$

Composition of cospans (i.e., of 1-cells)

$$(A \stackrel{f}{\to} B \stackrel{g}{\leftarrow} C) \; ; \; (C \stackrel{h}{\to} D \stackrel{k}{\leftarrow} E)$$

is obtained by taking the pushout of $g$ and $h$, and composing $f$ and $k$ with the pushout coprojections. The disjoint sum induces an obvious tensor product on cospans.

The category obtained by taking isomorphism classes of 1-cells is a symmetric monoidal category $\mathbf{Cospan}$ with duals, in which each object is dual to itself. This works in a manner dual to the situation for $\mathbf{Span}$, where the unit and counit are given by "equality predicates"; thus for each object $U$, the unit and counit of $U \dashv U$ are given by coequality cospans

$$\eta_U = (0 \to U \stackrel{\nabla_U}{\leftarrow} U + U), \qquad \epsilon_U = (U + U \stackrel{\nabla_U}{\to} U \leftarrow 0).$$

Thus, given a bijection $\sigma: A + U \to B + U$, the tracing $Tr_{A, B}^U(\sigma)$, given by a composite of cospans

$$A \cong A + 0 \stackrel{1_A + \eta_U}{\to} A + U + U \stackrel{\sigma + U}{\to} B + U + U \stackrel{1_B + \epsilon_U}{\to} B +0 \cong B,$$

can be read off by taking a pushout in $\mathbf{Set}$ of the diagram

$$A + U \stackrel{1_A + \nabla}{\leftarrow} (A + U + U \stackrel{\sigma + U}{\to} B + U + U \stackrel{1_B + \nabla_U}{\to} B + U) \qquad (1)$$

and then composing the pushout coprojections with the canonical inclusions $A \hookrightarrow A + U$, $B \hookrightarrow B + U$.

This gives a precise categorical description of the trace operation in terms of pushouts in $\mathbf{Set}$, but: it's the trace operation that pertains to the traced monoidal category denoted $\mathbf{Bij}'$ in the original post (where one keeps track of loops formed in the tracing process). If one wants to *ignore* loops that are formed by composing cospans, i.e., work with the traced monoidal category $\mathbf{Bij}$, one ought to work with *co-relations* instead of cospans.

By definition, a co-relation is a cospan $A \stackrel{f}{\to} C \stackrel{g}{\leftarrow} B$ such that the induced map $(f, g): A + B \to C$ is *epic*. In other words, a co-relation is a relation in the category $\mathbf{Set}^{op}$. One should pause to note that the power set functor $P: \mathbf{Set}^{op} \to \mathbf{Set}$ is monadic, and since a monadic category over $\mathbf{Set}$ is Barr exact and in particular a regular category, the usual calculus of relations goes through. In particular, to compose co-relations in $\mathbf{Set}$, one composes them as cospans but then one applies the epi-mono factorization to the composition cospan $(f, g): A + B \to C$; the epi part $q: A + B \to C'$ gives the composition co-relation. All the relevant structural features one had from $\mathbf{Cospan}$ carry over: $\mathbf{Corel}$ is a symmetric monoidal category in which each object is dual to itself, using the same formulas for the unit and counit of $U \dashv U$.

So, in summary, the result of the pushout (1) above induces a cospan from $A$ to $B$, and after applying the appropriate epi-mono factorization to get a co-relation, one can check that the result is a bijection from $A$ to $B$ (i.e., a cospan obtained by applying the inclusion functor $\mathbf{Bij} \hookrightarrow \mathbf{Corel}$ to a suitable bijection). This is the trace in $\mathbf{Bij}$.

It's not hard to see what is really going on. Tracing is basically the introduction of a feedback loop where outputs of $\sigma$ in $U$ are fed back in as inputs in $U$ living in $A + U$, and iterating through cycles until you exit $U$. That's exactly what the string diagram picture suggests (with the proviso that we are dealing with co-relation composition, which elides over free-floating loops where one never exits $U$). The meaning in terms of the cycle decomposition is hopefully clear. For instance, to take the example of the OP, we have in one of the cycles of $\sigma$ a path $5 \to 8$; this output $8 \in U$ is reinterpreted as an input where the next step in the cycle is $8 \to 3$, at which point we have exited out of $U$.

`retract_okounkov_vershik`

. Checking that the image is a permutation using my definition is not too hard: the inverse of the image of $\sigma$ is the image of $\sigma^{-1}$ (although the trace map is not a group morphism). – darij grinberg May 30 at 19:19