Getting rid of parameters

[andrejbauer]

There is currently quite a lot of confusion in the paper. I am going to list the problems I see, but it's probably a bad idea to try to fix each one separately without thinking of the paper as a whole. Here's one.

In Section 3, the higher inductive types H_rec, H_Con^n etc. are parameterized by P. This does not make sense, first because P is an expression schema, and also because we only ever introduce non-parameterized types.

I also find the entire construction very hard to follow because of the notation. It would be better to fix P and n and all the other things that the type depends on, and then not mention them in the names of constructions.

[nmvdw]

I agree. But if we don't put the parameter in the name, how can we distinguish between H_Con \> P and H_Con Q? Same way as now or a different notation?

[andrejbauer]

I can answer that once I understand what H_con P is :-)

[nmvdw]

H_Con P makes constructor terms of P. H_rec P is terms of depth 1 using the constructor c from the HIT and arguments from T. For H_Con we look at terms of depth at most n.