Homotopy Type Theory valuation (measure theory) > history (Rev #2)

Contents

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

Definition

In set theory

In measure theory, a valuation on a lattice (L,,,,,)(L, \leq, \bot, \vee, \top, \wedge) is a monotonic function μ:L[0,1]\mu:L \to [0, 1] such that μ()=0\mu(\bot) = 0 and the modularity condition is satisfied:

aL.bL.μ(a)+μ(b)=μ(ab)+μ(ab)\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,,,,,)(L, \leq, \bot, \vee, \top, \wedge) is a monotonic function μ:L[0,]\mu:L \to [0, \infty] with

  • a term ζ:μ()=0\zeta:\mu(\bot) = 0
  • a dependent family of terms
    a:L,b:Lm(a,b):μ(a)+μ(b)=μ(ab)+μ(ab)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

References

Revision on April 14, 2022 at 03:22:03 by Anonymous?. See the history of this page for a list of all contributions to it.