  The algebraic properties of the combination of probabilistic choice and
nondeterministic choice have long been a research topic in program semantics.
This paper explains a formalization in the Coq proof assistant of a monad
equipped with both choices: the geometrically convex monad. This formalization
has an immediate application: it provides a model for a monad that implements a
non-trivial interface which allows for proofs by equational reasoning using
probabilistic and nondeterministic effects. We explain the technical choices we
made to go from the literature to a complete Coq formalization, from which we
identify reusable theories about mathematical structures such as convex spaces
and concrete categories, and that we integrate in a framework for monadic
equational reasoning.
