Timeline for How is this fixed point theorem related to the axiom of choice?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 24, 2018 at 16:30 | comment | added | Tom Leinster | Andrej, as in my comment above (under the question), I don't think that's quite right. And as your nice paper makes clear, Bourbaki-Witt is provable without choice, whereas Andreas has just shown that this fixed point theorem isn't. By the way, we had some discussion of your paper and your earlier arXiv:0911.0068 back here. | |
| Dec 24, 2018 at 9:55 | comment | added | Andrej Bauer | For a constructive treatment of the theorem, see On the Bourbaki-Witt theorem in toposes (arXiv version). | |
| Dec 24, 2018 at 4:57 | comment | added | Andreas Blass | @TomLeinster You're right. The argument that works in general is the one using some $b'>b$. (Unfortunately I can't edit the comment to correct it.) | |
| Dec 24, 2018 at 0:32 | comment | added | Tom Leinster | Wonderful! Thank you. Just one thing: in your comment, I think you mean "the argument in the case $b \in C'$ works in general". | |
| Dec 24, 2018 at 0:31 | vote | accept | Tom Leinster | ||
| Dec 23, 2018 at 23:34 | history | edited | Andreas Blass | CC BY-SA 4.0 |
fixed a typo
|
| Dec 23, 2018 at 23:30 | comment | added | Andreas Blass | The case distinction as to whether $b\in C'$ is unnecessary; the argument in the case $b\notin C'$ works in general. In fact, It seems that the argument can be easily reformulated to also avoid using contraposition. Think of my answer as a "stream of consciousness" approximation to a cleaner, constructive (or at least much more constructive) version. | |
| Dec 23, 2018 at 23:26 | history | answered | Andreas Blass | CC BY-SA 4.0 |