# Monomorphic vs Polymorphic type theory

I am currently reading the book Programming in Martin-Löf type theory by Nordström et al. In the book they have two important parts, one about monomorphic set theory and the other about polymorphic set theory. Why do they do this? What are important differences. As far as I understand from the book monomorphic version reduces to polymorphic but not vice versa. Why is this so?

While polymorphic sets are the more traditional view, there is an argument that the way mathematicians actually reason is mostly monomorphic e.g. $\mathbb{R}\in 2$ is not a proposition that should make sense. These notes by Martin Löf may clarify matters a bit.