Predicate Transformers, (co)Monads and Resolutions

TL;DR

This paper explores a factorization theorem for closure and interior operators on powersets, relating it to resolutions in monads and comonads, with implications for formal topology and constructivity.

Contribution

It introduces a new factorization theorem connecting closure/interior operators with resolutions for monads and comonads, applicable constructively and classically.

Findings

The theorem holds constructively with variations.

Classically, the theorem often requires non-predicative interpolants.

Provides insights into formal topology and predicate issues.

Abstract

This short note contains random thoughts about a factorization theorem for closure/interior operators on a powerset which is reminiscent to the notion of resolution for a monad/comonad. The question originated from formal topology but is interesting in itself. The result holds constructively (even if it classically has several variations); but usually not predicatively (in the sense that the interpolant will no be given by a set). For those not familiar with predicativity issues, we look at a ``classical'' version where we bound the size of the interpolant.