nLab union structure

Contents

Definition

Given a set VV with an extensional relation \prec, a proto-union structure is a function U:VVU:V \to V such that

  • for all elements aVa \in V, bVb \in V, and cVc \in V, if aba \prec b and bcb \prec c, then aU(c)a \prec U(c).

Given a set VV with an extensional relation \prec, a union structure is a proto-union structure where additionally

  • for all elements aVa \in V and cVc \in V, if aU(c)a \prec U(c), then there exists bVb \in V such that aba \prec b and bcb \prec c.

Uniqueness of U(c)U(c) follows from \prec being an extensional relation.

Foundational concerns

In any material set theory, instead of postulating the mere existence of a set UU in which aba \in b and bcb \in c implies that aUa \in U, one could add a primitive unary operation U(c)U(c) which takes material sets cc and returns a material set U(c)U(c) such that for all aa and bb, aba \in b and bcb \in c implies that aU(c)a \in U(c).

 See also

Last revised on December 12, 2022 at 18:06:51. See the history of this page for a list of all contributions to it.