identity type usage

[DanGrayson]

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.

[mikeshulman]

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

[DanGrayson]

Isn't pq=91 a proposition?

[awodey]

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.

[awodey]

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

[mikeshulman]

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

[awodey]

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.

[mikeshulman]

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.

[DanGrayson]

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.

[mikeshulman]

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

[DanGrayson]

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.

[awodey]

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

[awodey]

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

[mikeshulman]

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

[awodey]

agreed.

[DanGrayson]

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

[awodey]

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

[DanGrayson]

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.

[mikeshulman]

What else could we be doing?

[DanGrayson]

It won't be obvious to students.