A <a href="http://ncatlab.org/nlab/show/measurable+space">measurable space</a> $(X,\mathcal X)$ consists of a set $X$ equipped with a $\sigma$-algebra of subsets $\mathcal X$. I would like to write computer programs involving measurable spaces, but to the best of my knowledge, no language (<a href="http://stackoverflow.com/questions/7123501/why-doesnt-haskells-data-set-support-infinite-sets">including Haskell</a>) has the ability to deal with completely unstructured sets. On the other hand, <a href="http://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html">type theory</a> is an alternate foundation for mathematics which is well-grounded computationally. 

Given a measurable space $(X,\mathcal X)$, is there an equivalent presentation using Martin-Löf dependent type theory?

With no constraints on the measurable space, the answer is probably no; a counterexample would be appreciated. What if $\mathcal X$ is a countably generated $\sigma$-algebra?