The ALEA Coq library formalizes discrete measure theory using a variant of the Giry monad, as a submonad of the CPS monad: (A -> [0,1]) -> [0,1]. This allows one to use Moggi's monadic meta-language to give an interpretation of a language, Rml, into type theory. Rml is a functional language with a primitive for probabilistic choice. This formalization was the semantical basis for the Certicrypt system for verifying security protocols. We improve on the formalization by using homotopy type theory which provides e.g. quotients and functional extensionality. Moreover, homotopy type theory allows us to use synthetic topology to present a theory which also includes "continuous" data types, like [0,1]. We also get a constructive formalization of probabilistic programming.