A measurable space $(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 (including Haskell) has the ability to deal with completely unstructured sets. On the other hand, type theory 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?