It would be nice if a theory could indicate that two colours are symmetric: swapping their roles across an entire diagram is always legal. It is the reality of the ZX calculus, and roughly halves the amount of axioms and proofs needed. Possibly this could be done by axiom, but that wouldn't reduce the amount of theorems, just make every second derivation easier.
Caveat: colour-swapped rules should not be tried by default (otherwise, bringing rules to normal form in simprocs becomes more difficult since we lose the "greenness" implicit metric, needing to specify it explicitly)
It would be nice if a theory could indicate that two colours are symmetric: swapping their roles across an entire diagram is always legal. It is the reality of the ZX calculus, and roughly halves the amount of axioms and proofs needed. Possibly this could be done by axiom, but that wouldn't reduce the amount of theorems, just make every second derivation easier.
Caveat: colour-swapped rules should not be tried by default (otherwise, bringing rules to normal form in simprocs becomes more difficult since we lose the "greenness" implicit metric, needing to specify it explicitly)