A correspondence between proximity homomorphisms and certain frame maps via a comonad - Ando Razafindrakoto (Categories and General Algebraic Structures with Applications)
We exhibit the proximity frames and proximity homomorphisms as a Kleisli category of a comonad whose underlying functor takes a proximity frame  to its frame of round ideals. This construction is known in the literature as stable compactification ([6]). We show that the frame of round ideals naturally carries with it two proximities of interest from which two comonads are induced.