Timeline for Defining computable functions categorically
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 18, 2018 at 6:29 | comment | added | Qiaochu Yuan | I think one has to say a bit more to fully answer the OP's question. Here's a start: suppose you have two PNNOs in a suitable category. Since PNNOs are defined by a universal property there is a unique isomorphism between them compatible with the inclusion of $1$ and the successor function. I think the OP's question is something like: what does it mean for this isomorphism itself to be computable? Or is this even a useful / interesting / meaningful question? | |
| May 18, 2018 at 4:00 | history | edited | François G. Dorais | CC BY-SA 4.0 |
corrections
|
| May 18, 2018 at 0:27 | comment | added | Andreas Blass | The $G$ described in the last sentence of your answer seems to be the relation defined by $f(\vec n,m)=0$, which need not be the graph of a function. You need to cut down $G$ to contain only one point per fiber; in other words, the projection from $G$ to $\mathbf N^k$ needs to be an isomorphism, not just a regular epi. | |
| May 17, 2018 at 21:25 | comment | added | François G. Dorais | Yes, @DavidRoberts, fixed now. | |
| May 17, 2018 at 21:25 | history | edited | François G. Dorais | CC BY-SA 4.0 |
added 2 characters in body
|
| May 17, 2018 at 20:52 | comment | added | David Roberts♦ | Is there a k missing in your commutative square? | |
| May 17, 2018 at 20:07 | history | answered | François G. Dorais | CC BY-SA 4.0 |