Dynamics and Coherence for the Free Cornering with Protocol Choice
arXiv:2508.00633
Abstract
We present a term rewriting system that models the dynamic aspects of the free cornering with protocol choice of a monoidal category, which has been proposed as a categorical model of process interaction. This term rewriting system is confluent and terminating in an appropriate sense. We use this machinery to prove a coherence theorem for the free cornering with protocol choice.
We have realised that the term rewriting system this paper concerns is not, in fact, confluent modulo equations. That is, proposition 16 (part 2) does not hold. This invalidates most of the development of the paper. We believe the problem to be unfixable, and have abandoned this particular line of work