A constructive Galois connection between closure and interior

Abstract

We construct a Galois connection between closure and interior operators on a given set. All arguments are intuitionistically valid. Our construction is an intuitionistic version of the classical correspondence between closure and interior operators via complement.

arXiv commentThis is a revised version. Content is reorganized so to separate clearly what requires an impredicative proof from what can be proven also predicatively. Moreover, some results are given in a more general form and some counterexamples are added