A Proof Sketch Of Something Which May Possibly Be A Conjecture of Oege de Moor

This note suports to prove something which Oege de Moor presented as an open problem in a talk entitled \Pointwise Relations” at the Computer Laboratory on December 1st. Since I’ve rephrased everything in terms with which I’m more familiar1 (and may well have misunderstood or misremembered what he said), it’s entirely possible that it doesn’t, however. Oege starts with a simply-typed lambda calculus. This is given two interpretations, one in Set and one in Rel . Now Rel is the Kleisli category of the powerset monad P on Set and I believe that Oege’s direct relational semantics is the same one as you get by factoring through the call-by-value translation into Moggi’s computational metalanguage and then interpreting that in Set with T = P