De Vries Powers and Proximity Specker Algebras

By de Vries duality, the category $$\textsf {KHaus}$$ KHaus of compact Hausdorff spaces is dually equivalent to the category $$\textsf {DeV}$$ DeV of de Vries algebras. There is a similar duality for $$\textsf {KHaus}$$ KHaus , where de Vries algebras are replaced by proximity Baer-Specker algebras. The functor associating with each compact Hausdorff space a proximity Baer-Specker algebra is described by generalizing the notion of a boolean power of a totally ordered domain to that of a de Vries power. It follows that $$\textsf {DeV}$$ DeV is equivalent to the category $$\text {\textsf{PBSp}}$$ PBSp of proximity Baer-Specker algebras. The equivalence is obtained by passing through $$\textsf {KHaus}$$ KHaus , and hence is not choice-free. In this paper we give a direct algebraic proof of this equivalence, which is choice-independent. To do so, we give an alternate choice-free description of de Vries powers of a totally ordered domain.