DPiepgrass comments on Basic building blocks of dependent type theory

[DPiepgrass]

Please don’t defend the “∏” notation.

$$f:\prod _{x:X}Y$$

It’s nonsensical. It implies that

$$\lambda (x:N).x$$

has type ” ∞! × 0″!

[Dacyn]

How so? It looks like you have confused ${\prod }_{x:X}Y$ with ${\prod }_{x:X}x$. In this example we have $X=Y=N$, so the type of $\lambda (x:N).x$ is ${\prod }_{x:N}N$.

[DPiepgrass]

Pardon me. I guess its type is $N^{\infty }$.