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?
$\begingroup$
$\endgroup$
0
asked Apr 30, 2014 at 20:03
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
As far as I understand it, the notion of polymorphic set denotes sets which are primitive, in other words which are first-order objects that can be manipulated, and such that set membership is a predicate, elements can be members of multiple sets. In monomorphic sets, sets are interpreted as predicates on types, and membership of a type is a jugement. In particular, a term can only be a member of a single set (up to equality of types).
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.
