[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] The objects of our theory are called functions. In addition, it comes with * A binary predicate $(-)=(-)$ called *equality* * for all functions $f$, $f = f$ * for all functions $f$ and $g$, $f = g$ implies that $g = f$ * for all functions $f$, $g$, and $h$, $f = g$ and $g = h$ imply that $f = h$ * A unary predicate $\mathrm{set}(-)$ called *being a set* * A unary operator $\mathrm{dom}(-)$ called the *domain* of a function * for all functions $f$, $\mathrm{set}(\mathrm{dom}(f))$. * A unary operator $\mathrm{codom}(-)$ called the *codomain* of a function * for all functions $f$, $\mathrm{set}(\mathrm{codom}(f))$. * A unary predicate $\mathrm{element}(-)$ called *being an element* * A binary predicate $(-)\in(-)$ called *membership* * if $a \in b$, then $a$ is an element and $b$ is a set $$\forall a.\forall b.(a \in b) \to \mathrm{element}(a) \wedge \mathrm{set}(b)$$ * if $a \in b$, then $\mathrm{dom}(b) = \mathrm{codom}(a)$ * extensionality for sets and elements: for all $a$ and for all $b$, if a and b are sets, then $a = b$ if and only if, for all $c$, if $c$ is an element, then $c \in a$ if and only if $c \in b$ $$\forall a.\forall b.(\mathrm{set}(a) \wedge \mathrm{set}(b)) \implies ((a = b) \iff \forall c.(\mathrm{element}(c) \implies ((c \in a) \iff (c \in b))))$$ * for all $f$ and $x$ where $\mathrm{element}(x)$ and $x \in \mathrm{dom}(f)$, there exists a $y$ such that $\mathrm{element}(y)$ and $y \in \mathrm{codom}(f)$ * A constant $1$ called the *singleton* or the *point*. * $\mathrm{set}(1)$ and $\mathrm{element}(1)$ * for all $f$, $\mathrm{set}(f)$ implies that $\mathrm{codom}(f) = 1$ and $\mathrm{dom}(f) = f$. * for all $f$, $\mathrm{element}(f)$ implies that $\mathrm{dom}(f) = 1$. * for all $A$ and $B$ such that $\mathrm{set}(A)$ and $\mathrm{set}(B)$, there exists a $C$ such that $\mathrm{set}(C)$, a $\pi_1^C$ with $\mathrm{dom}(\pi_1^C) = c$ and $\mathrm{codom}(\pi_1^C) = A$, a $\pi_2^C$ with $\mathrm{dom}(\pi_2^C) = C$ and $\mathrm{codom}(\pi_2^C) = B$, such that for all elements $a$ and $b$ where $a \in A$ and $b \in B$, there is an element $c$ where $c \in C$, category: redirected to nlab