A constructive Galois connection between closure and interior
Logic
2012-03-23 v2 Category Theory
General Topology
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.
Cite
@article{arxiv.1101.5896,
title = {A constructive Galois connection between closure and interior},
author = {Francesco Ciraulo and Giovanni Sambin},
journal= {arXiv preprint arXiv:1101.5896},
year = {2012}
}
Comments
This 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