If a locale is presented by a “flat site”, it is shown how its frame can be presented by generators and relations as a dcpo. A necessary and sufficient condition is derived for compactness of the locale . Although its derivation uses impredicative constructions, it is also shown predicatively using the inductive generation of formal topologies. A predicative proof of the binary Tychonoff theorem is given, including a characterization of the finite covers of the product by basic opens. The discussion (...) is then related to the double powerlocale. (shrink)

The paper studies how the localic notion of sublocale transfers to formal topology. For any formal topology (not necessarily with positivity predicate) we define a sublocale to be a cover relation that includes that of the formal topology. The family of sublocales has set-indexed joins. For each set of base elements there are corresponding open and closed sublocales, boolean complements of each other. They generate a boolean algebra amongst the sublocales. In the case of an inductively generated formal topology, the (...) collection of inductively generated sublocales has coframe structure. Overt sublocales and weakly closed sublocales are described, and related via a new notion of "rest closed" sublocale to the binary positivity predicate. Overt, weakly closed sublocales of an inductively generated formal topology are in bijection with "lower powerpoints", arising from the impredicative theory of the lower powerlocale. Compact sublocales and fitted sublocales are described. Compact fitted sublocales of an inductively generated formal topology are in bijection with "upper powerpoints", arising from the impredicative theory of the upper powerlocale. (shrink)

An account of lower and upper integration is given. It is constructive in the sense of geometric logic. If the integrand takes its values in the non-negative lower reals, then its lower integral with respect to a valuation is a lower real. If the integrand takes its values in the non-negative upper reals, then its upper integral with respect to a covaluation and with domain of integration bounded by a compact subspace is an upper real. Spaces of valuations and of (...) covaluations are defined.Riemann and Choquet integrals can be calculated in terms of these lower and upper integrals. (shrink)

The locale corresponding to the real interval [ − 1, 1] is an interval object, in the sense of Escardó and Simpson, in the category of locales. The map, mapping a stream s of signs ±1 to, is a proper localic surjection; it is also expressed as a coequalizer. The proofs are valid in any elementary topos with natural numbers object.