# Contents * table of contents {: toc} In [[categorical set theories]] such as [[ETCS]], the set theory is usually a theory of [[sets]] and [[functions]] in an abstract category, with [[elements]] being defined as the [[global elements]], the [[morphisms]] out of the [[terminal object]]. However, this approach poses a few issues, namely that in ordinary mathematical practice, elements are not the same as functions out of the terminal object, although they are isomorphic to each other, and function evaluation of elements in categorical set theories are an abuse of notation. There are other [[structural set theories]], such as [[SEAR]], which explicitly put in the elements of a set as a primitive of the theory: this is equivalent to saying that the category is an [[concrete category]] rather than an abstract category. In such a presentation involving sets and functions, [[function evaluation]] would be an external version of an [[evaluation map]] defined on the concrete category, making the category into an [[evaluational category]], and the axiom of function extensionality is defined directly on the elements, rather than the global element morphisms out of the terminal object. The presentation of such a concrete categorical set theory reads more like a traditional presentation of set theory in terms of sets and elements, rather than category theory. In this presentation, we will be adapting Tom Leinster's presentation of ETCS to the concrete setting. Some of these axioms might be redundant, but that was true of Tom Leinster's original presentation. ## Basic primitives ## Our theory has the following primitives: * Some things called **sets**; * For every set $A$, these things called **elements in $A$**, with elements $a$ in $A$ written as $a \in A$; * For every set $A$ and $B$, these things called **functions from $A$ to $B$**, with functions $f$ from $A$ to $B$ written as $f:A \to B$; * For every set $A$ and $B$, an operation called **function evaluation** assigning every element $a \in A$ and function $f:A \to B$ an element $f(a) \in B$; * For every set $A$, a function $id_A:A \to A$ called the **identity function of $A$**; * For every set $A$, $B$, and $C$, an operation called **function composition** assigning every function $f:A \to B$ and $g:B \to C$ a function $g \circ f:A \to C$; ## Equality of elements and functions ## For every set $A$ and elements $a \in A$ and $b \in A$, there is a relation $a = b$ called **equality of elements**, such that * for every element $a \in A$, $a = a$ * for every element $a \in A$ and $b \in A$, $a = b$ implies that $b = a$ * for every element $a \in A$, $b \in A$, and $c \in A$, $a = b$ and $b = c$ implies that $a = c$. For every set $A$ and $B$ and functions $f:A \to B$ and $g:A \to B$, there is a relation $f = g$ called **equality of functions**, such that * for every function $f:A \to B$, $f = f$ * for every function $f:A \to B$ and $g:A \to B$, $f = g$ implies that $g = f$ * for every function $f:A \to B$, $g:A \to B$, and $h:A \to B$, $f = g$ and $g = h$ implies that $f = h$. ## Basic axioms for functions ## **Axiom of identity functions.** For every set $A$ and for every element $a \in A$, $id_A(a) = a$. **Axiom of currying.** For every set $A$, $B$, and $C$, and for every element $a \in A$, $(g \circ f)(a) = g(f(a))$. **Axiom of extensionality.** For every set $A$ and $B$ and for every function $f:A \to B$ and $g:A \to B$, if $f(x) = g(x)$ for all elements $x \colon A$, then $f = g$. The associativity and unit laws of function composition follow from the axioms: * For every set $A$ and $B$, function $f:A \to B$, and element $a \in A$, $$(g \circ id_A)(a) = g(id_A(a)) = g(a)$$ and extensionality implies that $g \circ id_A = g$. * For every set $A$ and $B$, function $f:A \to B$, and element $a \in A$, $$(id_B \circ g)(a) = id_B(g(a)) = g(a)$$ and extensionality implies that $id_B \circ g = g$. * For every set $A$, $B$, $C$, and $D$, function $f:A \to B$, $g:B \to C$, and $h:C \to D$, and element $a \in A$, $$(h \circ (g \circ f))(a) = h((g \circ f)(a)) = h(g(f(a)) = (h \circ g)(f(a)) = ((h \circ g) \circ f)(a)$$ and extensionality implies that $h \circ (g \circ f) = (h \circ g) \circ f$. Thus, these axioms imply that the collection of sets, functions, and elements form a [[concrete category]] that is [[evaluational category|evaluational]] and [[extensional category|extensional]]. Those who are versed in [[type theory]] would recognize that the axiom of currying as an instance of [[currying]] a function $f:((B \to C) \times (A \to B)) \to A$ to a function $f^{'}:(B \to C) \to ((A \to B) \to A)$, hence the name of the axiom. ## Singletons ## **Axiom of singletons.** There is a set $\mathbb{1}$, called a **singleton**, with a unique element $* \in \mathbb{1}$, called a **point**. $\mathbb{1}$ is a terminal set, in the sense that for every set $A$, there is a unique function $f:A \to \mathbb{1}$. This is because $\mathbb{1}$ only has a unique element in it. This implies that for every element $a \in A$ and every function $f:A \to \mathbb{1}$ and $g:A \to \mathbb{1}$, $f(a) = *$ and $g(a) = *$, which by extensionality implies that $f = g$. Therefore, every two functions from $A$ to $\mathbb{1}$ are equal, and so there is a unique function from $A$ to $\mathbb{1}$. ## Cartesian products ## **Axiom of Cartesian products.** For every set $A$ and $B$, there is a set $P$, called a **Cartesian product** of $A$ and $B$, with a function $p_A:P \to A$ called the **projection onto $A$** and a function $p_B:P \to B$ called the **projection onto $B$**, such given two elements $a \in A$ and $b \in B$ there is a unique element $(a, b) \in P$ such that $p_A((a, b)) = a$ and $p_B((a, b)) = b$. The structure consisting of sets $C$, $A$, and $B$, with a pair of functions $f:C \to A$ and $g:C \to B$ is called a **span** between $A$ and $B$. A Cartesian product $P$ of $A$ and $B$ with functions $p_A:P \to A$ and $p_B:P \to B$ is a terminal span between $A$ and $B$, in the sense that for every other span $(C, f:C \to A, g:C \to B)$, there is a unique function $h:C \to P$ such that for all elements $c \in C$, $p_A(h(c)) = f(c)$ and $p_B(h(c)) = g(c)$. This is because a Cartesian product $P$ ## Fibers ## ... ## Function sets ## ... ## Set of truth values ## ... ## Set of natural numbers ## ... ## Choice sets ## ... ## References ## * [[Tom Leinster]], Rethinking set theory, ([arxiv:1212.6543](https://arxiv.org/abs/1212.6543))