BTW, have you see the new paper The constrained-monad problem? I want to investigate whether its techniques can apply to Category & friends for linear maps and for circuits. Perhaps you’d like to give it a try as well. I got to linear maps as an elegant formulation of timing analysis for circuits.