The connected Vietoris powerlocale

The connected Vietoris powerlocale is defined as a strong monad V c on the category of locales. V c X 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 × : V c X × V c Y → V c ( X × Y ) shows that the product of two strongly connected sublocales is strongly connected. If X is locally connected then V c X is overt. For the localic completion Y ¯ of a generalized metric space Y, the points of V c Y ¯ are certain Cauchy filters of formal balls for the finite power set F Y with respect to a Vietoris metric. ation to the point-free real line R gives a choice-free constructive version of the Intermediate Value Theorem and Rolleʹs Theorem. rk is topos-valid (assuming natural numbers object). V c is a geometric construction.