- 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 sets $A$ and $B$, the **bijection set** $\mathrm{Bij}(A, B)$ is the set of bijections between the set $A$ and $B$. In the foundations of mathematics, the existence of such a set may be taken to follow from the existence of power sets, from the axiom of subset collection, from the existence of function sets, from the existence of injection sets, or as an axiom (the **axiom of bijection sets**) in its own right.

If the set theory has function sets, then the bijection set between $A$ and $B$ is a subset of the function set between $A$ and $B$: $\mathrm{Bij}(A, B) \subseteq B^A$. Similarly, if the set theory has injection sets, then the bijection set between $A$ and $B$ is a subset of the injection set between $A$ and $B$: $\mathrm{Bij}(A, B) \subseteq \mathrm{Inj}(A, B)$

The bijection set between $A$ and itself is the symmetric group on $A$, $\mathrm{Sym}(A) \coloneqq \mathrm{Bij}(A, A)$.

In the context of the axiom of choice or stronger axioms such as a choice operator satisfying the axiom schemata of existence, having bijection sets implies having power sets in the foundations, since the axiom of choice implies that for every set $A$, there is a bijection $\mathcal{P}(A) \cong \mathrm{Sym}(A)$ between the power set of $A$ and the symmetric group on $A$. Thus, bijection sets are a form of impredicativity from the point of view of mathematics with the axiom of choice.

The universal property of the bijection set states that given a function $X \to \mathrm{Bij}(A, B)$ from a set $X$ to the bijection set between sets $A$ and $B$, there exists a bijection $A \times X \cong B \times X$ in the slice category $\mathrm{Set}/X$.

Thinking of Set as a locally small category, this is a special case of the hom-set of the core of Set.

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

Last revised on January 10, 2023 at 20:54:43. See the history of this page for a list of all contributions to it.