- fundamentals of set theory
- material set theory
- presentations of set theory
- structuralism in set theory
- class-set theory
- constructive set theory
- algebraic set theory

Given a set $V$ with an extensional relation $\prec$ on $V$, a **pairing structure** is a binary function $P:V \times V \to V$ such that

- for all $a \in V$ and $b \in V$, $a \prec P(a, b)$ and $b \prec P(a, b)$

An **unordered pairing structure** on $V$ is pairing structure $\{-,-\}:V \times V \to V$ where additionally

- for all sets $z$, $z \in \{x, y\}$ implies that $z = x$ or $z = y$.

Uniqueness of $\{x, y\}$ follows from $\prec$ being an extensional relation.

An **ordered pairing structure** on $V$ is a pairing structure $(-,-):V \times V \to V$ which satisfies product extensionality:

- for all $a \in V$, $a' \in V$, $b \in V$, $b' \in V$, $P(a, b) = P(a', b')$ if and only if $a = a'$ and $b = b'$

In any material set theory, instead of postulating the mere existence of a set $P$ in which $a \in P$ and $b \in P$ one could add a primitive binary operation $P(a, b)$ which takes material sets $a$ and $b$ and returns a material set $P(a, b)$ such that for all $a$ and $b$, $a \in P(a, b)$ and $b \in P(a, b)$

- Håkon Robbestad Gylterud, Elisabeth Bonnevier,
*Non-wellfounded sets in HoTT*(arXiv:2001.06696)

Last revised on December 15, 2022 at 22:50:33. See the history of this page for a list of all contributions to it.