Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
This page says:
Its induction principle says that for any equipped with a point and a dependent path , there is such that:
Should it instead say , or , or “dependent path over ”, or something like that? Does it matter?
Adrian
I think that’s right, there is a transport involved. That’s what the link dependent path is referring to. For the moment i have added (here) the missing -subscript and a pointer to UFP13, p. 177.
Ideally I would like to polish up the whole presentation (which is due to the notorious “Anonymous”, in revision 5) but not now.
On whether it matters: I expected it does. While I haven’t tried to write out a formal argument, a quick idea goes as follows:
In the higher induction principle of the suspension type there is certainly such dependent identifications involved, namely along the two “meridian” paths from the “north pole” to the “south pole”: by the general rules of higher inductive types, but also because here it would not even type-check otherwise. But then for the evident map to be an equivalence, there must be a corresponding dependent identification also in the induction principle of .
1 to 9 of 9