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:S1→Type equipped with a point base′:P(base) and a dependent path loop′:base′=base′, there is f:∏(x:S1)P(x) such that:
Should it instead say loop′:trloopP(base′)=base′, or loop′:base′=loopPbase′, 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 SS0 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 S1→SS0 to be an equivalence, there must be a corresponding dependent identification also in the induction principle of S1.
Assuming that the computation rule for the basepoint of S1 is propositional, the propositional computation rule for the loop of S1 listed on the page in the section titled “In natural deduction” is wrong. The application of the dependent function indS1(c*,c𝓁) defined in the elimination rule of S1 to the loop identification 𝓁:*=S1* is actually in the heterogeneous identity type
indS1(c*,c𝓁)(*)=𝓁̲.CindS1(c*,c𝓁)(*)rather than the heterogeneous identity type c*=𝓁̲.Cc*. One needs to transport the application across the identification β*S1(c*,c𝓁):indS1(c*,c𝓁)(*)=C(*)c* found in the propositional computation rule for the basepoint *:S1 in order for everything to type check in the propositional computation rule for the loop, or otherwise use a heterogeneous identity type instead of a homogeneous identity type, like
β𝓁S1(c*,c𝓁):apdindS1(c*,c𝓁)(𝓁)=β*S1(c*,c𝓁)̲.(−)=𝓁̲.C(−)c𝓁The term “identification type” is the more logically consistent one, though.
The term “identification type” is the more logically consistent one, though.
If you prefer, I could use “identification type” throughout the article instead of “identity type”. The problem is that originally the article used both “identification type” and “identity type”.
I added an explanation for the inference rules for the circle type, similar to the explanation for the inference rules for identity types over in that article.
1 to 19 of 19