#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 __valuation__ on a [[lattice]] $(L, \leq, \bot, \vee, \top, \wedge)$ is a [[monotonic function]] $\mu:L \to [0, 1]$ such that $\mu(\bot) = 0$ 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 __valuation__ on a [[lattice]] $(L, \leq, \bot, \vee, \top, \wedge)$ is a [[monotonic function]] $\mu:L \to [0, \infty]$ with * a term $\zeta:\mu(\bot) = 0$ * 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 ## * [[probability valuation]] * [[sigma-continuous valuation]] ## References ## * Alex Simpson, [Measure, randomness and sublocales](https://www.sciencedirect.com/science/article/pii/S0168007211001874).