HoTT
identity type usage
Here is an example where an identity type is used in a sentence as though it were a proposition:
This is likely to cause confusion.
Don't we do this all throughout mathematics? "There are prime numbers p and q such that pq = 91."
The correct form of elimination and computation rules for the higher constructors of HITs is a somewhat delicate matter - and still open to different approaches. See section 6.2 for a discussion of some of the issues. Note that in CTT the computation rule for loop is also definitional.
We could reduce possible confusion by referring back to Lemma 6.25, and recall the issues by writing (more correctly): f(base) :== b ap_f(loop) := L
The book doesn't reserve "proposition" to refer to only (-1)-types; it calls those "mere propositions".
MS: "The book doesn't reserve "proposition" to refer to only (-1)-types; it calls those "mere propositions"." good point! I think a compromise also determined that it's ok to simply display a (general) type, i.e. one that's not a mere proposition, and say that it "holds" (or similar) to mean that it's inhabited.
Right. I don't think there's any potential ambiguity in that; what else could it mean?
There is a bit of lack of parallelism in these sentences of the form "such that P and Q" where P is a judgment and Q is a type, but I don't think that's very serious.
I think a compromise also determined that it's ok to simply display a (general) type, i.e. one that's not a mere proposition, and say that it "holds" (or similar) to mean that it's inhabited.
In the paragraph I highlighted above, you don't want to assert that the type is inhabited, you want to give an element of it.
Giving an element of a type is the same as asserting that it is inhabited. (Not to be confused with asserting that it is merely inhabited!)
Oops, you're right -- indeed, you say this: "when we say that A is inhabited, we mean that we have given a (particular) element of A, but that we are choosing not to give a name to that element" in 1.11.
true. But the convention (I guess) is that simply displaying a type such as a = b means the same as the judgement that the type is inhabited (or rather, the meta-statement that there is some t for which the judgement t : a = b holds).
that in response to MS: "There is a bit of lack of parallelism in these sentences of the form "such that P and Q" where P is a judgment and Q is a type, but I don't think that's very serious."
If that's to be the convention, then this paragraph should probably be extended to explain it to the reader:
It should be explained that when you write "if X", or when you assert "X", you are regarding X as a proposition, in the way described.