Timeline for Where in ordinary math do we need unbounded separation and replacement?
Current License: CC BY-SA 3.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 11, 2013 at 19:15 | vote | accept | Andrej Bauer | ||
| Feb 11, 2013 at 7:07 | comment | added | David Roberts♦ | Yes, I meant in the general context of the page you link to, rather than arbitrary endofunctors on arbitrary categories. | |
| Feb 11, 2013 at 6:02 | comment | added | Andrej Bauer | Computer scientists like initial algebras of functors, and if they don't have to think about their existence they feel a bit like physicists who are allowed to differentiate everything they like. | |
| Feb 11, 2013 at 1:39 | comment | added | Todd Trimble | @David: of course many endofunctors do not have free algebras at all. That aside, it is certainly convenient to have a global result such as theorem 1 here: ncatlab.org/nlab/show/transfinite+construction+of+free+algebras, and I'm not sure one can prove that without a replacement scheme in the background set theory. But you're right that significant instances of such a result can be proven in say ETCS (without replacement); e.g., I think existence of free algebras for "polynomial" endofunctors is no problem. The small object argument is probably a good acid-test case to consider. | |
| Feb 10, 2013 at 22:51 | comment | added | David Roberts♦ | And in 'ordinary mathematics', does one use an arbitrary endofunctor and need to construct free algebras? In all 'ordinary cases' wouldn't we have some sort of properties of the category at hand/objects of the category at hand/the endofunctor that allows a workaround? | |
| Feb 10, 2013 at 21:06 | comment | added | Andrej Bauer | Yes, I think often I don't need replacement in a constructive setting because I have available suitable inductive constructions. | |
| Feb 10, 2013 at 19:51 | history | answered | Todd Trimble | CC BY-SA 3.0 |