🪄 New hcom syntax with inference

[ralsei]

[The title of this PR is pretty bad... I'm not sure exactly what to call this change still!]

This PR adds a new syntax for hcom, in which the type and cofibration are read off the goal type and its boundary (so, when the goal is a sub). A demo of this used wherever possible is given in the provided test file bruno.cooltt, a formalization of much of Cubical informal type theory: the higher groupoid structure by Bruno Bentzen.

The motivation for this is that leading into the graphical editor project, we want the user to have to enter as little information as possible when the computer writes an hcom for them.

This is currently very WIP. Namely, as discussed, the tactical hcom_chk needs to fix the "local soundness" property mentioned by Jon to qualify as a good Chk tactic. In addition, the near-identical hfill syntax is presently nonfunctional.

[ralsei]

Current things that need to be fixed:

• [ ] This would be a lot easier if hcom was a Chk tactic. We can do this by dropping a hole when hcom doesn't satisfy the boundary, and then removing the hole :sparkles: magically :sparkles: when the boundary is satisfied. I think this UX is generally better, and should probably apply for other similar Syn tactics like coe.
• [x] HFillInfer complains about needing a true cofibration. I am not sure why.
• [x] Sometimes, HComInfer infers the wrong cofibration (in the case of bruno.cooltt, ∂ i instead of ∂ i ∨ ∂ k. This is probably because the subtype is not the only source of boundary necessary. I am not sure where to get the ∂ k from.
• [ ] This might still break the local soundness invariant mentioned. I don't fully understand the theory, so I'm relying on external insight for that.
• [ ] If we're dropping magic boundary holes, maybe we shouldn't show boundary holes in the pretty printer, and instead display a different error that's more "hole-like" than a hole itself.

[ralsei]

I think that the hcom et al as a Chk tactic can be worked with later, so I'm putting this up for review.

[jonsterling]

I will do my best to review this today.