identity type usage about book HOT 19 OPEN

Don't we do this all throughout mathematics? "There are prime numbers p and q such that pq = 91."

from book.

Isn't pq=91 a proposition?

from book.

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.

from book.

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

from book.

The book doesn't reserve "proposition" to refer to only (-1)-types; it calls those "mere propositions".

from book.

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.

from book.

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.

from book.

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.

from book.

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!)

from book.

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.

from book.

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).

from book.

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."

from book.

Right, that's why I think it's not very serious.

from book.

agreed.

from book.

If that's to be the convention, then this paragraph should probably be extended to explain it to the reader:

from book.

Why isn't that just what that paragraph already explains?

from book.

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.

from book.

What else could we be doing?

from book.

It won't be obvious to students.

from book.