<p>As far as I understand it, the notion of <em>polymorphic set</em> denotes sets which are <em>primitive</em>, in other words which are first-order objects that can be manipulated, and such that set membership is a <em>predicate</em>, elements can be members of multiple sets. In monomorphic sets, sets are interpreted as predicates on <em>types</em>, and membership of a type is a <em>jugement</em>. In particular, a term can only be a member of a <strong>single set</strong> (up to equality of types).</p>

<p>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. <a href="http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf" rel="nofollow">These notes</a> by Martin Löf may clarify matters a bit.</p>

CC BY-SA 3.0
2014-05-02T14:04:35.513Z
2014-05-02T14:04:35.513Z
cody
<p>I am currently reading the book <a href="http://www.ens-lyon.fr/denif/data/martin_lof_prog/1990/contenu/book.pdf" rel="nofollow">Programming in Martin-Löf type theory</a> 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?</p>

<lo.logic><type-theory>
Monomorphic vs Polymorphic type theory
Konstantin Solomatov
# Monomorphic vs Polymorphic type theory

(Asked by: username_0 on 2014-04-30)

I am currently reading the book [Programming in Martin-Löf type theory](http://www.ens-lyon.fr/denif/data/martin_lof_prog/1990/contenu/book.pdf) 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?

**Tags:** lo.logic, type-theory

---

## 1 answers

### Answer by username_1 on 2014-05-02. Score: 4 | Accepted answer

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](http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf) by Martin Löf may clarify matters a bit.


---

