Prerequisites: Algebraic General Topology.
Describing a cartesian closed category such that Top and the category of proximity spaces would be its full subcategories, would probably lead to some significant progress of mathematics.
Victor Porton proposes that the category cont(mepfFcd) (the category of continuous monovalued, entirely defined pointfree funcoids) may be such a category. See this draft for the definition of cont(mepfFcd).
But proving that cont(mepfFcd) is cartesian closed category (particularly that binary products exist in this category) stumbles over an open problem:
Victor Porton conjectures that the following function is a product morphism for pointfree funcoids , (at least in the case when , are monovlaued and entirely defined funcoids):
The main trouble is that it is not known that such a pointfree funcoid exists. So proving its existence would be probably very important.
We could use a theorem from this article (currently numbered "Theorem 53") which states existence of a pointfree funcoid having certain values on ultrafilters, but the theorem has too strong conditions. (Can we lessen the theorem conditions?)