When building nontrivial proofs in homotopy.io, the hardest technique is performing nontrivial expansions. For example, consider trying to build the naturality move for the attached scenario.
Type checking is so fast now there's something better we could do. When clicking a vertex of the diagram, the tool could isolate that as a subdiagram D, and then enumerate all "interesting" expansion rewrites R:E--->D. (So the system would have to build both R and E.) It would build some candidates up to a certain size, and then type check them, presenting the valid ones to the user to choose from. With the correct heuristics in place this could enable a vast range of useful moves to be done in a single click (naturality, braiding conversion in a symmetric monoidal category).
This would be the first AI technique for homotopy.io, I'm sure there's a ton of other things that could be done like this.
jamievicary
commented
2 years ago
When building nontrivial proofs in homotopy.io, the hardest technique is performing nontrivial expansions. For example, consider trying to build the naturality move for the attached scenario.
Type checking is so fast now there's something better we could do. When clicking a vertex of the diagram, the tool could isolate that as a subdiagram D, and then enumerate all "interesting" expansion rewrites R:E--->D. (So the system would have to build both R and E.) It would build some candidates up to a certain size, and then type check them, presenting the valid ones to the user to choose from. With the correct heuristics in place this could enable a vast range of useful moves to be done in a single click (naturality, braiding conversion in a symmetric monoidal category).
This would be the first AI technique for homotopy.io, I'm sure there's a ton of other things that could be done like this.
naturality.zip