As the title said, I would like to know if constructive measure theory has been developed somewhere ?
I am more precisely interested in the (constructive) theory of completely continuous valuation on locale, or eventually in countably continuous valuation on locale.
I know how to do constructively the integration of positive lower semi-continuous function with respect to a positive valuation (with value in lower semi-continuous real number) and I want to know if this kind of things has already been written properly somewhere (in order to be quoted) ?
On a closely related subject, I also want to know if the fact that the set of projection of an abelian von-neuman algebra $A$ is a frame whose corresponding locale $NSp A$ is the classifying space of the theory of normal character of $A$ and that complex valued function on $NSp A$ can be identified with unbounded operator affiliated to $A$ has been already written properly somewhere ? (I often see these mentioned in article or on MO, but I have never see a 'quotable' proof published. )
PS : By 'constructively' I mean using intuitionist logic.
Thank you !