search

nmvdw / Three-HITs

All higher inductive types can be obtained from three simple HITs.
17 stars 2 forks source link

Types of paths in computation rule for paths #12

Open andrejbauer opened 7 years ago

andrejbauer commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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