A finitely presented finitary discrete 2-theory holds some hope of being computationally tractable. With regards to the free algebra that such a structure generates, I'll ask (and answer): Is there a decision procedure for the commutativity of diagrams? (Yes with an "if") Can we always find a finite set of diagrams whose commutativity imply the commutativity of all others? (No with a "but")