Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In set theory

In measure theory, a measure on a $\sigma$-frame or more generally a $\sigma$-complete distributive lattice $(L, \leq, \bot, \vee, \top, \wedge, \Vee)$ is a valuation $\mu:L \to [0, \infty]$ such that the elements are mutually disjoint and the probability valuation is denumerably/countably additive

In homotopy type theory

In measure theory, a measure on a $\sigma$-frame or more generally a $\sigma$-complete distributive lattice $(L, \leq, \bot, \vee, \top, \wedge, \Vee)$ is a valuation $\mu:L \to [0, \infty]$ with

• a family of dependent terms
  $$s:\mathbb{N} \to L \vdash \alpha(s):\left(\prod_{m:\mathbb{N}} \prod_{n:\mathbb{N}} (m \neq n) \times (s(m) \wedge s(n) = \bot)\right) \times \left(\mu(\Vee_{n:\mathbb{N}} s(n)) = \sum_{n:\mathbb{N}} \mu(s(n)) \right)$$

  representing the mutually disjoint elements condition and the denumerably/countably additive condition.

See also

• sigma-frame

• sigma-complete lattice

• distributive lattice

• valuation (measure theory)

• sigma-continuous valuation

• probability measure

References

• Alex Simpson, Measure, randomness and sublocales.