Make definition of ε-net use zero-based indexing

[Bolpat]

Sounds big, but it’s basically just a typo. Zero-based indexing is actually used later when an $ε$-net is defined as

$$x_i=i/k\text{\quad for }i=0,\dots,k$$

in the proof of Theorem 11.5.6.
And it makes sense considering $\mathbb N$ contains $0$.

[mikeshulman]

Hmm, I actually prefer it the current way. The way it is currently, n is the length of the finite list of points forming the epsilon-net, and when n=0 the list is empty. I would prefer to change the proof of 11.5.6 to say $x_i = (i-1)/k$ for $i=1,\dots,k+1$.

[Bolpat]

The zero-based indexing is also used in:

• the definition of a totally bounded metric space (in Definition 11.5.3, directly after the definition of $ε$-net, indirectly by using $∃(k≤n). d(x_k,y)<ε$ which would have to change to $∃(k≤n). k>0 ∧ d(x_k,y)<ε$;
• the proof of Theorem 11.5.7, there are $h(ϵ)$-net $y_0, \dots{}, y_n$ and the $h(η)$-net $z_0, \dots{}, z_m$ mentioned, where $0$ could be replaced by $1$ easily, as far as I can tell.

After taking a closer look, for $M$ empty, the empty list is actually needed because there is no other $\mathrm{List}(M)$ in that case. Both the indexing base and the empty case can be solved in spirit of Remark 11.5.4, only that I’d suggest we use the vector types $\mathrm{Vec}_n(M)$ defined in § 5.7 Generalizations of inductive types.

Definition 11.5.3. […]
A metric space $(M, d)$ is totally bounded when it has $ϵ$-nets of all sizes:

$$\prod_{(ϵ:\mathbb Q_+)} \sum_{(n:\mathbb N)} \sum_{(x:\mathrm{Vec}_n(M))} ∀(y:M). ∃(k:\mathrm{Fin}(n)). d(x_k,y) < ε.$$

Remark 11.5.4. In the definition of total boundedness we used the notation $x_k$ to index into the vector $x$ at $k$. Formally, we should have defined an indexing operator by recursion:

$$\begin{align} \mathrm{index}: \prod_{(A:\mathcal U)} \prod_{(n:\mathbb N)} \mathrm{Vec}_n(A) → \mathrm{Fin}(n) & → A \\\ (A,n+1,\mathrm{cons}_{n+1}(a, x), 0_n) & \mapsto a \\\ (A,n+1,\mathrm{cons}_{n+1}(a, x), (k+1)_{n+1}) & \mapsto \mathrm{index}(A,n,x,k_n) \end{align}$$

Of course, we leave $A$ and $n$ implicit and write $x_k$ for $\mathrm{index}(x,k)$. There is no case for $n=0$ since $\mathrm{Fin}(0)$ is empty.

What do you think of this?

[mikeshulman]

I don't think there is any need to change the notation by introducing vectors; Remark 11.5.4 is sufficient as a nod towards precision. This is informal type theory after all. (-:

[mikeshulman]

I also don't think it's necessary to add k>0 to the statements: since we already aren't explicitly mentioning what type k belongs to, it might as well be the type of positive integers.