Andrej Bauer: There are no intuitionistic space-filling curves

Abstract: A space-filling curve is a continuous surjection from the closed interval onto a space. Such a curve was first constructed by Giuseppe Peano in 1890. In 1913, Hans Hahn and Stefan Mazurkiewicz independently characterized the spaces which can be filled by a curve as the compact, connected, locally connected, metrizable inhabited Hausdorff spaces.

We show that in intuitionistic logic with countable choice the usual constructions of space-filling curves work as expected. Consequently, such curves are computable and computably surjective. The use of countable choice is essential – in the topos of sheaves over the closed square there is no square-filling curve, which means that there can be no purely intuitionistic square-filling curve.