The Connected Vietoris Powerlocale

The connected Vietoris powerlocale is defined as a strong monad Vc on the category of locales. VcX is a sublocale of Johnstone's Vietoris powerlocale VX, a localic analogue of the Vietoris hyperspace, and its points correspond to the weakly semifitted sublocales of X that are “strongly connected”. A product map ×:VcX×VcY→Vc(X×Y) shows that the product of two strongly connected sublocales is strongly connected. If X is locally connected then VcX is overt. For the localic completion of a generalized metric space Y, the points of are certain Cauchy filters of formal balls for the finite power set with respect to a Vietoris metric. Application to the point-free real line gives a choice-free constructive version of the Intermediate Value Theorem and Rolle's Theorem. The work is topos-valid (assuming natural numbers object). Vc is a geometric construction