milestone.  proved galois connection between monotonic, proper function spaces.  lots of setoids, quotienting, and type classes involved, but the result is very elegent.