It should be not too hard to write a solver for wild categories (might still be that I am missing some detail which causes a problem in the end...). I have the following scheme in mind, but there might be others:
[ ] Construct the free wild category on a reflexive graph (partially done with #1117 )
[ ] An equation between compositions of morphisms in a wild category is a (reflexive) diagram which is the boundary of a 2-cell.
[ ] Use the universal property to construct a filler of this 2-cell if the compositions are equal in the free wild cat.
[ ] Build a nice reflection interface.
Feel free to discuss this scheme and suggest improvements!
It should be not too hard to write a solver for wild categories (might still be that I am missing some detail which causes a problem in the end...). I have the following scheme in mind, but there might be others:
Feel free to discuss this scheme and suggest improvements!