The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tuesday, January 28, 2014 06:55:39 AM Arnaud Spiwack wrote:
> Indeed. And in fact, there is also the singleton monad, whose Kleisli
> category is the category of functional relations.

Hmm, and what would the Eilenberg-Moore category be?  Maybe something like 
the 
category of types with a unique choice operator -- which I guess isn't that 
interesting after all since the only such constructible operators I can think 
of is on unit, empty types, or products of types in the image of singleton.
-- 
Daniel Schepler