Elsevier, Electronic Notes in Theoretical Computer Science, (319), p. 37-49, 2015
DOI: 10.1016/j.entcs.2015.12.004
Full text: Download
The notion of trace in a monoidal category has been introduced to give a categorical account of a situation occurring in very different settings: linear algebra, topology, knot theory, proof theory... with the trace operation understood as a feedback operation. Partially traced categories were later introduced to account for cases where the trace is not always defined, and it was shown that partially traced category can always be seen as a subcategory of a totally traced one. We give a new proof of this representation theorem, using a construction that is different from the original one. However, since they satisfy the same universal property they are naturally isomorphic.