The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Well, precisely. An algebra A on S, the singleton monad, is given by a ι:S A -> A, such that ι{a} = a (the product condition is vacuous, since S A is isomorphic to S (S A)). Algebra morphism are just regular functions. That's a definition of a definite choice operator. As per types that support such an operator, there are the sub-singleton types too. So it may still be of use.

On 28 January 2014 17:44, Daniel Schepler <dschepler AT gmail.com> wrote:

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