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 $P:S^1\to Type$ equipped with a point $base' : P(base)$ and a dependent path $loop':base'= base'$, there is $f:\prod_{(x:S^1)} P(x)$ such that:
Should it instead say $loop' : tr^{loop}_P(base') = base'$, or $loop' : base' =^{loop}_{P} base'$, or “dependent path $loop':base'= base'$ over $loop$”, 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 $=_{loop}$-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 $\mathrm{S}S^0$ 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 $S^1 \to \mathrm{S}S^0$ to be an equivalence, there must be a corresponding dependent identification also in the induction principle of $S^1$.
1 to 9 of 9