This PR removes the support for cartesian structure from the solver, but exchanges it for the ability to render an expression into pure structure, meaning the context can be wiped clean as structural rewrites are being applied.
At the moment, because cartesian structures aren't recognized, this means that fork f g will be represented simply as Morph 5 (depending on the environment), which is useless for the purpose of rewriting. Somehow the solver will need to recognize and reflect many different kinds of morphisms, but without incurring so many dependencies that it's only usable in specific scenarios.
This PR removes the support for cartesian structure from the solver, but exchanges it for the ability to render an expression into pure structure, meaning the context can be wiped clean as structural rewrites are being applied.
At the moment, because cartesian structures aren't recognized, this means that
fork f gwill be represented simply asMorph 5(depending on the environment), which is useless for the purpose of rewriting. Somehow the solver will need to recognize and reflect many different kinds of morphisms, but without incurring so many dependencies that it's only usable in specific scenarios.