Timeline for Why in Martin-Löf type theory any natural number is assumed to be either $0$ or $S(a)$ for some $a\in\mathsf{N}$?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 11, 2022 at 14:33 | vote | accept | qk11 | ||
| Jan 10, 2022 at 22:03 | comment | added | Andrej Bauer | I already invented another notation, and implemented it in an experimental proof assistant that support abstraction as a primitive operation, it's $\{n\}\{y\} f$. I am not sure it's any good though, it uses up $\{$ and $\}$. | |
| Jan 10, 2022 at 21:38 | comment | added | Andreas Blass | Oh, so the dot after $ny$ functions like a $\lambda$ or rather a pair of $\lambda$'s, but understood in a dependent-type sense where the type of $y$ depends on $n$. Since some people still use dots for simple grouping, I"d encourage you to invent another notation. (By the way, I'm not a fan of $\lambda$ either, since most mathematicians would not write $\lambda x t$ but rather $x\mapsto t$.) | |
| Jan 10, 2022 at 21:30 | comment | added | Andrej Bauer | Oh no, that's a binder. It binds $n$ and $y$ simulatneously, so they do not roam freely when they shouldn't. We lack good standard notation for such things. | |
| Jan 10, 2022 at 21:27 | comment | added | Andreas Blass | In the last rule, the one for rec, I think $ny$ is a typo. | |
| Jan 10, 2022 at 21:21 | history | answered | Andrej Bauer | CC BY-SA 4.0 |