Add support for holes

[smimram]

Often, when I construct a proof, I want to try to fill "part of the diagram". Would it be possible to add a symbol _ which would be able to take any type so that I could be able to start typing "partial morphisms" and the defined part is still typechecked?

[thibautbenjamin]

This should be doable using unification,
however, it raises the question of how this should be integrated with some kind of UI. Easy choice would be to add holes and call catt on the file, and have catt stop the first term with holes and display the type inferred type for the holes.

More advanced strategies to integrate that more naturally could be a thing, like with agda. Similarly to agda, I suggest the symbol ? to designate holes, as _ already denotes an argument that can be inferred automatically