Dacyn comments on Basic building blocks of dependent type theory

Dacyn 6 Jan 2023 17:33 UTC
1 point
0
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 $λ (x : N) . x$ is $\prod_{x : N} N$ .
- DPiepgrass 25 Jan 2023 6:39 UTC
  1 point
  0
  Parent
  Pardon me. I guess its type is $N^{\infty}$ .