#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In set theory ### In measure theory, a __probability valuation__ on a [[lattice]] $(L, \leq, \bot, \vee, \top, \wedge)$ is a [[monotonic function]] $\mu:L \to [0, 1]$ such that $\mu(\bot) = 0$, $\mu(\top) = 1$, and the modularity condition is satisfied: $$\forall a \in L. \forall b \in L. \mu(a) + \mu(b) = \mu(a \wedge b) + \mu(a \vee b)$$ ### In homotopy type theory ### In measure theory, a __probability valuation__ on a [[lattice]] $(L, \leq, \bot, \vee, \top, \wedge)$ is a [[monotonic function]] $\mu:L \to [0, 1]$ with * a term $\zeta:\mu(\bot) = 0$ * a term $\omega:\mu(\top) = 1$ * a dependent family of terms $$a:L, b:L \vdash m(a, b):\mu(a) + \mu(b) = \mu(a \wedge b) + \mu(a \vee b)$$ representing the modularity condition. ## See also ## * [[unit interval]] * [[valuation (measure theory)]] * [[sigma-continuous probability valuation]] ## References ## * Alex Simpson, [Measure, randomness and sublocales](https://www.sciencedirect.com/science/article/pii/S0168007211001874).