Footnote 66 explaining the first ! (bang)

[marcbezem]

The first use of ! (the Big Bang of the bang, so to say) occurs on p. 44 and is explained in footnote 66:

"Elements of a type that is a proposition carry no information beyond witnessing that the proposition is non-empty, since all elements of a proposition can be identified. Therefore we may replace them by an exclamation mark."

Should we leave out "carry no information beyond witnessing that the proposition is non-empty"? After all, such elements can carry information, such as about a center of contraction, or the number of elements in a finite type. It is true that all other elements of the type that is a proposition carry the same information, but that is something else than carrying no information.

Also, this use of ! is such an important convention that it deserves a more prominent announcement, perhaps already in 2.15?

[DanGrayson]

Yes, a witness to contractibility provides the center of contraction. But then, any element of the contractible type is the center of a contraction. So in some sense, it carries no information. Well, it provides an element of the type, which might not be available otherwise.

(Being a finite type is not a proposition.)

[marcbezem]

I was thinking of Lemma 2.24.4(1), concerning finite types. Here comes an example.

Define f: Π(X:U) ((Σ(n:N) || X = [n] ||) -> N) by f(X,(n,!)) :≡ n. Even though the type of (n,!) is a proposition, it seems difficult to define f(X,!), if at all possible. One gets an interesting variant by truncating the Σ-type. Since N is not a proposition, you need to factor through the Σ-type, which is a proposition, and then use f.

Thinking about the pedagogy of this, taking into account that there are very few uses of ! in Ch. 2, it may be better to postpone this convention till Ch. 3. In any case, I would feel more comfortable with the following explanation of the convention:

"Since all elements of a proposition are equal, it is often not necessary to name such elements explicitly. If the proposition in question is clear from the context, we may use ! as a default name of its elements. Be warned that different occurrences of ! may refer to elements of different propositions. In cases where the element of a proposition is not of interest (beyond its mere existence), we may even just ignore it. For example, we do this when we speak of a proof p of an element P of Prop. Here we mean (P,!) : Prop and p : P."

We may add as an example the function f above, with the truncated variant as an exercise.

[marcbezem]

Progress report: I removed "!" from Ch. 2 (just a few) and have moved on to Ch. 3, looking for a good place to introduce this (very convenient) convention. When I have found that place I'll let you know and then the issue can be closed if you are all happy with my solution.

[marcbezem]

Found a good place, see dd66a46. It is currently (version 23.08) Remark 3.5.1, with \label{rem:bang}. I close the issue, but feel free to reopen it if you would like to discuss it further.