Spreads and choice in constructive mathematics. (Q1866471)

To avoid using countable choice in a constructive existence proof, the author argues for constructing a spread in which all finite paths possess the desired property. A single object with this property is then an infinite path, which can be chosen only by countable choice. This generalises the author's treatment of the fundamental theorem of algebra [Pac. J. Math. 196, 213--230 (2000; Zbl 1046.03036)]. Among other things, it is linked to the basic concept of point-free topology: to deal with ideal, infinite objects only through real, finite approximations or observables.