Higher inductive types

[jonweinb]

This is to raise some thoughts on the possibility of having higher inductive types in the future, even just for paths to begin with (so in the Standard HoTT sense).

For example, having pushouts would enable to treat a closure property of left orthogonal maps as well as alternative characterizations of Rezk types via the construction of the free bi-invertible arrow as in [BW23, Subsection 4.2.1].

[alexandre-emmanuel]

I would like to take this issue, but I am only beginner and I am actively studying the field. So, if there are some advice or roadmap (or very focused article), then it would be helpful to hear. As I understand, having HITs we will be able to formalize limits and that is the important ingredient for the ∞-topos and hence - quite general semantics of HoTT.

I understand that I need to extend the syntax, parser and rules, but it can be possible that these things can be borrowed e.g. from cubical Agda?

[fizruk]

@alexandre-emmanuel Hi there! Thanks for suggesting your help. On the surface, the roadmap seems relatively straightforward:

1. Propose syntax extension, covering both HIT declarations (with appropriate validity checks), as well as introduction and elimination of HIT values. We can take inspiration from Cubical Agda, of course. I would suggest to also have some directed HITs in mind for future to avoid scraping the syntax when we would want to add those.
2. Extend grammar and internal well-scoped AST.
3. Add HIT info with computation rules to the typing/evaluation context.
4. Implement typechecking with HITs (should be straightforward).
5. Implement validity checks for HITs (can be pretty conservative at first).

I would expect elimination to cause most problems for the implementor (in the beginning at least):

• Elimination can implemented with as dependent pattern matching, but it might be difficult to do that immediately (it is not a trivial task).
• With the current implementation of Rzk it might be easier to generate an induction principle with corresponding computation rules instead.
• We can actually already #postulate induction principle, so we may have poor man's HITs, if only we could also have user-defined computation rules

So if you want to be able to define a few HITs and then use them in proofs, rather than have a general safe support for HITs, then the best option, in my opinion, would be to simply offer user-defined computation rules (see Agda's Rewriting for inspiration as well). To do that, I think it would be enough to postulate a computation rule as a propositional equality and then have a command that turns that equality into a computation rule. You can see here an example of postulating a (regular) inductive types (coproducts, booleans, naturals).

Of course, general rewrite rules break many things, but I believe it is good to have them anyway, while confluence and termination checks can (and should) be added later.