Types of paths in computation rule for paths

[andrejbauer]

Coq is asking me why the left and the right side of the equation at the bottom of page 3 (the one that says 'apD Hrec (p_i a) = q_i a (Bi Hrec a)`) have the same type. Is this supposed to be obvious?

In the formalization we'll have to insert a transport becaue the computation rule for points is not judgmental (we can't express judgmental equality like that), but I'd first like to understand why the equation is supposed to make sense in the paper.

In concrete examples the types seem to match, although (somwhat amazingly), all point constructors in the HoTT library that I could find were non-recursive and so they're much more easily handled.

[nmvdw]

It is not, but I did not recall it in the paper. We proved that in Proposition 13 in the paper 'Higher Inductive Types in Programming'. http://www.jucs.org/jucs_23_1/higher_inductive_types_in/jucs_23_01_0063_0088_basold.pdf

[andrejbauer]

Ok good, then we can turn Proposition 13 into a propositional equality in the formalization.