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$.
Assuming that the computation rule for the basepoint of $S^1$ is propositional, the propositional computation rule for the loop of $S^1$ listed on the page in the section titled “In natural deduction” is wrong. The application of the dependent function $\mathrm{ind}_{S^1}(c_*, c_\mathcal{l})$ defined in the elimination rule of $S^1$ to the loop identification $\mathcal{l}:* =_{S^1} *$ is actually in the heterogeneous identity type
$\mathrm{ind}_{S^1}(c_*, c_\mathcal{l})(*) =_{\underline{ }.C}^{\mathcal{l}} \mathrm{ind}_{S^1}(c_*, c_\mathcal{l})(*)$rather than the heterogeneous identity type $c_* =_{\underline{ }.C}^{\mathcal{l}} c_*$. One needs to transport the application across the identification $\beta_{S^1}^{*}(c_*, c_\mathcal{l}):\mathrm{ind}_{S^1}(c_*, c_\mathcal{l})(*) =_{C(*)} c_*$ found in the propositional computation rule for the basepoint $*:S^1$ 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
$\beta_{S^1}^{\mathcal{l}}(c_*, c_\mathcal{l}):\mathrm{apd}_{\mathrm{ind}_{S^1}(c_*, c_\mathcal{l})}(\mathcal{l}) =_{\underline{ }.(-) =_{\underline{ }.C}^{\mathcal{l}} (-)}^{\beta_{S^1}^{*}(c_*, c_\mathcal{l})} c_\mathcal{l}$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 18 of 18