Introduce indexed-subset notation

[mikeshulman]

Do we formally introduce the notation { f(x) | x:A } anywhere, for a function f : A -> B between sets? It doesn't seem to be in section 3.7, which would be the logical place for it, since it has to mean { y:B | \exists x:A. f(x) = y }. If we add this, then we should refer back to it in places where it is used much later, like Lemma 10.3.7 (pointed out by @martinescardo).

[martinescardo]

Maybe it is not enough to point out just this. In the proof of Lemma 10.3.7, we have {f'(a,s(a')) | a' < a}. (*)

This seems to mean {b | ∥Σ (a' : A), Σ (l : a' < a), f' a' (s a' l) ≡ b∥}. (**)

It is important here that {...|...} is not a Sigma type (like in Coq), but the lambda-abstraction

λb , ∥Σ (a' : A), Σ (l : a' < a), f' a' (s a' l) ≡ b∥}.

Even if the notations {x : X |...} and {f x : Y | ...} (to mean lambda-abstractions) are introduced, this doesn't imply that when we write (*) we mean (**).

[mikeshulman]

I said that it has to mean something involving \exists, i.e. a truncation -- otherwise it's not a "subset" in the sense of section 3.5. I think this entails that (*) means (*), at least modulo the minor abuse of writing a' < a to mean `a':A (a' < a)`.

[martinescardo]

I think this is a major abuse.

[mikeshulman]

This sort of thing is totally standard in informal mathematics.

[martinescardo]

a' < a is a type quite different from a':A * (a' < a).

[mikeshulman]

Sure, but a' has to be bound to make the expression make any sense, and this way of binding it is the only sensible one.