As before, let S be the Stone locale of square roots of the generic complex number. The question is, In what sense can S be considered finite? Here is one idea that occurs to me. If a set is acted on transitively by a finite group, then classically it must be finite (and I dare say some constructive statement of this is also true). S is acted on by the discrete group {+1, -1} (by multiplication in C). Hence if that action can be considered transitive in some way, that would be a finiteness property of S (or, rather, finiteness _structure_ on S). If a: S x {+1, -1} -> S is the action, then I believe I can prove (by techniques involving the upper powerlocale) that <fst, a> : S x {+1, -1} -> S x S is a proper surjection. This would seem to be a natural way to capture transitivity of a and hence a finiteness property of S. More generally, if an action on a locale by a finite group has only finitely many orbits (using the above idea to specify transitivity on the orbits), then that would be a finiteness property of the locale. One might ask whether, by Galois theory, this can be applied to arbitrary polynomials over C. Steve Vickers.