Solver for wild categories
Opened this issue · 0 comments
felixwellen commented
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!