{-
\import Algebra.Monoid
\import Algebra.Pointed
\import Analysis.Measure.MeasureSpace
\import Arith.Real
\import Arith.Real.LowerReal
\import Function.Meta
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Set.Subset
\import Topology.CoverSpace
\open Bounded(bottom)
\open LowerReal

\class ValuationSpace \extends CoverSpace
  | valuation {U : Set E} : isOpen U -> LowerReal
  | valuation-empty : valuation open-bottom = 0
  | valuation-<= {U V : Set E} (Uo : isOpen U) (Vo : isOpen V) : U ⊆ V -> valuation Uo <= valuation Vo
  | valuation-modular {U V : Set E} (Uo : isOpen U) (Vo : isOpen V) : valuation (open-union Uo Vo) + valuation (open-inter Uo Vo) = valuation Uo + valuation Vo

\func MeasureToValuation (X : CoverSpace) (M : MeasureSpace X) : ValuationSpace X \cowith
  | CoverSpace => X
  | valuation {U} _ => BJoin 0 {Given (V : isMeasurable) (V ⊆ U)} \lam S => measure S.2
  | valuation-empty => <=-antisymmetric (BJoin-univ <=-refl \lam S => RealAbGroup.lower_<=-char.2 $ transport (_ <=) M.measure-empty $ M.measure-<= S.3) BJoin-bound
  | valuation-<= _ _ U<=V => BJoin-univ {0} BJoin-bound \lam S => BJoin-cond {0} $ later (S.1, S.2, S.3 <=∘ U<=V)
  | valuation-modular Uo Vo => {?}
 -}