How do we express measurable spaces using type theory?
If you clarify your question, I can modify this answer to be better. (I am sure you won't like my answer. The best answer is this is not practical, except in the simplest of settings. Or you are interested in this from a logical perceptive, in which case you need to learn the background. Or you care about probability, in which case the usual sigma-algebras are not the way to go.)
Question: What do you mean by presentation?
There are many meanings of a presentation of a mathematical object. Almost all mathematical objects can be represented in type theory. So a trivial answer is yes, you can represent measure spaces in type theory. Given a type $X$, you can make a new type $\mathtt{SigmaAlgebra}(X)$ that depends on $X$, and can be understood as the sigma-algebras of $X$. Rather than going into the details, it is important to note that this is all a formalism. If I know nothing about $X$ then I only know the most basic properties about $\mathtt{SigmaAlgebra}(X)$.
Update: Here is a clarification of the last paragraph. Type theory can be used as a foundation of mathematics. This is the foundations used in formal theorem provers including HOL Light, Isabelle, and Coq. The last one is most closely related to Martin-Löf type theory. It is possible to define a type $\mathtt{SigmaAlgebra}(X)$ by taking all elements of type $X \rightarrow \mathtt{Bool} \rightarrow \mathtt{Bool}$ (that is the powerset of the powerset of $X$) that are closed under the axioms of sigma-algebras. It is difficult to explain if you have never seen a formal theorem prover before, so I might suggest you learn one if you are really interested in this.
However, if you are looking to take any measurable space, and encode it as a specific representation (finitely-many bits of the computer memory), then of course it is not possible. There are way too many sigma-algebras to represent each as a finite bitstring in a computer. Not just more than countable, more than continuum many sigma-algebras on the reals for example.
Question: What do you want to do with these sigma-algebras?
You could be talking about formal theorem proving, but I assume you want to compute with these objects. Is this computation for probability or descriptive set theory? The choice of ideal computable representations is very different in each case.
Also, this brings me to my next question?
Question: What do you want to compute?
What are you going to do with these spaces? Did you want to construct the sigma-algebra generated by a collection of sets? Did you want to see if a particular set is in the sigma-algebra? Did you want to see if two sigma-algebras are equal? Did you want to define maps and ask where certain points map to? Did you want to compare elements of a sigma-algebra to see if they are the same?
With out answers to the above, I can't give you much help. But here are two ways to theoretically represent measurable spaces.
Approach 1: Assume $X$ is a complete separable metric space. Then $X$ can be represented by the distances between some dense countable subset (think the rationals in the reals). This is an infinite object, so you need to represent it as a function which on inputs $i,j,k$ gives the distance between the $i$th and $j$th "rational point" up to an error of $2^{-k}$.
Then you can represent each Borel set by its Borel code. Again, you can really only represent the Borel sets that have computable codes, since the code may be infinite. Again this representation is a function which returns Borel codes.
Then you can represent countably generated sigma-algebas that are subsets of the Borel sigma algebra, by taking a computable sequence of Borel sets, and using them as the representation of the sigma algebra.
However, this has many problems. I can't tell if two sigma algebras are the same. I can't tell if two sets are the same, I can't tell if a set is in a sigma-algebra. Hence, there isn't much that can be computed about this object.
Approach 2: (I am being quite sketchy on the details.) Assume there is also a probability measure. Just assume it is the Lebsegue measure on the unit interval. Then you can represent measurable sets (up to a.e. equivalence) by how close the set is to each finite union of rational intervals. The metric of "closeness" used is $d(A,B) = \mu (A \triangle B)$ where $\triangle$ is the symmetric difference.
Now define a sigma-algebra (up to a.e. equivalence) by the operator $f \mapsto \mathbb{E}[f\mid\mathcal{X}]$ which can be viewed as an operator from $L^2$ to $L^2$ for example (this can be made computable). While I don't want to go into the details, this has an advantage that one can ask if a set $A$ is an element of $\mathcal{X}$. While you can't get a perfect answer, you can get an approximation to a number between 0 and 1. Were $0$ is yes, and anything else is no.
If I really needed to compute with sigma-algebras in a probability theory context, I would do something like this.
Update: Here is an update to my answer based on the details that you gave about your project in your comment below. It looks like you would like to consider a space $X$, and then the space $\mathcal{M}_1(X)$ of probability measures on $X$, and then the space $\mathcal{M}_1(\mathcal{M}_1(X))$ and so on.
This is doable from a computational prospective assuming $X$ is a computable metric space and $\mathcal{M}_1(X)$ is the space of Borel probability measures on $X$. Examples of computable metric spaces include $\{0,1\}^\mathbb{N}$ (good for coin flipping), $C([0,1])$ (good for Brownian motion and continuous path processes), the RCCL functions on $[0,1]$ under the Stockenrod metic (good for RCLL processes), $R^\mathbb{N}$ (for real-valued discrete time Markov chains) and much more.
Given a computable metric space $X$, the space $\mathcal{M}_1(X)$ of Borel probability measures is also a computable metric space. The metric is the Levy-Prokohorov metric (which is a bit of a pain to work with). Also, one can represent the measures by their integrals, which are continuous linear operators on the bounded continuous functions. This represents the same topology. A good resource is "Computability of probability measures and Martin-Löf randomness over metric spaces" by Hoyrup and Rojas (you can skip the stuff about randomness for your needs) and "Representing Probability Measures using Probabilistic Processes" by Matthias Schröder and Alex Simpson (mentioned in another answer). The too papers have equivalent approaches.
Indeed, while I don't know if epistemic game theory has been looked at from a computational prospective, I know that related concepts like conditional probability, de Finetti's theorem, and nonparametric Bayesian statistics have been looked at using the theory of computable metric spaces and computable probability measures. Dan Roy's website is a good place to begin.
I am not exactly sure what you are looking for. There is this work in inductively generated sigma-algebras in type theory: http://link.springer.com/article/10.1007%2Fs001530100123
More generally, I would be inclined to an algebraic approach to measure theory.
For instance, using Riesz spaces (of real valued measurable functions modulo zero measure)
http://logicandanalysis.org/index.php/jla/article/view/14/12
or the related pointfree (localic) approach
http://www.cs.bham.ac.uk/~sjv/Riesz.pdf
http://homepages.inf.ed.ac.uk/als/Research/Sources/mrs.pdf
There is also these formalizations in type theory:
https://www.lri.fr/~paulin/ALEA/ (randomized algorithms)
http://www.cs.unibo.it/~sacerdot/PAPERS/jfr.pdf (Lebesgue’s Dominated Convergence Theorem in Matita).
I'd be happy to elaborate, but would need some more information about what you are searching about.
You might also be interested in this paper, which also points to many of the relevant works in the literature.
Matthias Schröder and Alex Simpson , "Representing Probability Measures using Probabilistic Processes"
Journal of Complexity, 22: 768--788, 2006.
Special Issue on Computability, Complexity and Analysis.
Available here: http://homepages.inf.ed.ac.uk/als/Research/Sources/JoCcca05.pdf