nLab union structure

\tableofcontents

Definition

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

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

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