[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \tableofcontents ## Presentation We present William Lawvere's Elementary Theory of the Category of Sets as [[first order logic]] over [[type theory]]. ### Judgments and contexts The judgments of this type theory consists of * Set judgments: $\Gamma \vdash A \; \mathrm{set}$ * Function judgments: $\Gamma \vdash f:A \to B$. The set $A$ is called the [[domain]] of the function $f$ and the set $B$ is called the [[codomain]] of $f$ * Proposition judgments: $\Gamma \vert \Phi \vdash A \; \mathrm{prop}$ * Truth judgments: $\Gamma \vert \Phi \vdash A \; \mathrm{true}$ There are contexts in general, and set contexts. Set contexts are defined in the usual way, as a list of function judgments: $$\frac{}{() \; \mathrm{setctx}} \qquad \frac{\Gamma \; \mathrm{setctx} \quad \Gamma \vdash A \; \mathrm{set} \quad \Gamma \vdash B \; \mathrm{set}}{(\Gamma, f:A \to B) \; \mathrm{setctx}}$$ And contexts are defined as a list of set contexts followed by a list of true propositions $$\frac{\Gamma \; \mathrm{setctx}}{\Gamma \vert () \; \mathrm{ctx}} \qquad \frac{\Gamma \vert \Phi \; \mathrm{ctx} \quad \Gamma \vert \Phi \vdash A \; \mathrm{prop}}{\Gamma \vert (\Phi, A \; \mathrm{true}) \; \mathrm{ctx}}$$ ### Predicate logic We begin with the type formers for propositions: these include [[true]], [[false]], [[disjunction]], [[conjunction]], and [[implication]]. A [[predicate]] is a proposition which depends on a function $$\Gamma, f:A \to B \vdash P \; \mathrm{prop}$$ and here are the type formers for the [[universal quantifier]]. $$\frac{\Gamma, x:A \to B \vdash P \; \mathrm{prop}}{\Gamma \vdash \forall x:A \to B.P \; \mathrm{prop}}$$ $$\frac{\Gamma, x:A \to B \vdash P \; \mathrm{true}}{\Gamma \vdash \forall x:A \to B.P \; \mathrm{true}}$$ $$\frac{\Gamma \vdash f:A \to B \quad \Gamma \vdash \forall x:A \to B.P \; \mathrm{true}}{\Gamma \vdash P[f/x] \; \mathrm{true}}$$ We could also include similar type formers for the [[existential quantifier]] as well. A [[binary relation]] is a proposition which depends on two functions $$\Gamma, f:A \to B, g:C \to D \vdash P \; \mathrm{prop}$$ a binary relation is homogeneous or an endorelation if the two function have the same domain and codomain $$\Gamma, f:A \to B, g:A \to B \vdash P \; \mathrm{prop}$$ ### Equality The [[equality]] in ETCS is a local homogeneous binary relation, and is formed by the following rule: $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set} \quad \Gamma \vert \Phi \vdash B \; \mathrm{set} \quad \Gamma \vert \Phi \vdash f:A \to B \quad \Gamma \vert \Phi \vdash g:A \to B}{\Gamma \vert \Phi \vdash f =_{A \to B} g \; \mathrm{prop}}$$ Equality also satisfies reflexivity, symmetry, and transitivity, making it into a equivalence relation $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set} \quad \Gamma \vert \Phi \vdash B \; \mathrm{set} \quad \Gamma \vert \Phi \vdash f:A \to B}{\Gamma \vert \Phi \vdash f =_{A \to B} f \; \mathrm{true}}$$ $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set} \quad \Gamma \vert \Phi \vdash B \; \mathrm{set} \quad \Gamma \vert \Phi \vdash f:A \to B \quad \Gamma \vert \Phi \vdash g:A \to B \quad \Gamma \vert \Phi \vdash f =_{A \to B} g \; \mathrm{true}}{\Gamma \vert \Phi \vdash g =_{A \to B} f \; \mathrm{true}}$$ $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set} \quad \Gamma \vert \Phi \vdash B \; \mathrm{set} \quad \Gamma \vert \Phi \vdash f:A \to B \quad \Gamma \vert \Phi \vdash g:A \to B \quad \Gamma \vert \Phi \vdash h:A \to B \quad \Gamma \vert \Phi \vdash f =_{A \to B} g \; \mathrm{true} \quad \Gamma \vert \Phi \vdash g =_{A \to B} h \; \mathrm{true}}{\Gamma \vert \Phi \vdash f =_{A \to B} h \; \mathrm{true}}$$ ### Identity functions and composition of functions In addition, there are specific functions representing the identity function of the set, and function composition of two functions, which is written in diagrammatic order: $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set}}{\Gamma \vert \Phi \vdash \mathrm{id}_{A}:A \to A}$$ $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set} \quad \Gamma \vert \Phi \vdash B \; \mathrm{set} \quad \Gamma \vert \Phi \vdash C \; \mathrm{set} \quad \Gamma \vert \Phi \vdash f:A \to B \quad \Gamma \vert \Phi \vdash g:B \to C}{\Gamma \vert \Phi \vdash \mathrm{comp}_{A, B, C}(f, g):A \to C}$$ which satisfy the left and right unital laws and the associative laws: $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set} \quad \Gamma \vert \Phi \vdash B \; \mathrm{set} \quad \Gamma \vert \Phi \vdash f:A \to B}{\Gamma \vert \Phi \vdash \mathrm{comp}_{A, A, B}(\mathrm{id}_{A}, f) =_{A \to B} f \; \mathrm{true}}$$ $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set} \quad \Gamma \vert \Phi \vdash B \; \mathrm{set} \quad \Gamma \vert \Phi \vdash f:A \to B}{\Gamma \vert \Phi \vdash \mathrm{comp}_{A, B, B}(f, \mathrm{id}_{B}) =_{A \to B} f \; \mathrm{true}}$$ $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set} \quad \Gamma \vert \Phi \vdash B \; \mathrm{set} \quad \Gamma \vert \Phi \vdash C \; \mathrm{set} \quad \Gamma \vert \Phi \vdash D \; \mathrm{set} \quad \Gamma \vert \Phi \vdash f:A \to B \quad \Gamma \vert \Phi \vdash g:B \to C \quad \Gamma \vert \Phi \vdash h:C \to D}{\Gamma \vert \Phi \vdash \mathrm{comp}_{A, C, D}(\mathrm{comp}_{A, B, C}(f, g), h) =_{A \to D} \mathrm{comp}_{A, B, D}(f, \mathrm{comp}_{B, C, D}(g, h)) \; \mathrm{true}}$$ ### Terminal set and elements There is a specified set $1$ called the terminal set. $$\frac{\Gamma \vert \Phi \; \mathrm{ctx}}{\Gamma \vert \Phi \vdash 1 \; \mathrm{set}}$$ The terminal set is characterised by the [[universal property]] that there is a unique function from every set $A$ to $1$, given by the following rules: $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set}}{\Gamma \vert \Phi \vdash u_A:A \to 1}$$ $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set} \quad \Gamma \vert \Phi \vdash a:A \to 1}{\Gamma \vert \Phi \vdash a =_{A \to 1} u_A \; \mathrm{true}}$$ An element $a$ of a set $A$ is a function $a:1 \to A$ whose domain is the terminal set and whose codomain is $A$. ### Function extensionality The axiom of [[function extensionality]] states that two functions $f:A \to B$ and $g:A \to B$ are equal if their composition with every element of $A$ is equal. It is given by the following rule: $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set} \quad \Gamma \vert \Phi \vdash B \; \mathrm{set} \quad \Gamma \vert \Phi \vdash f:A \to B \quad \Gamma \vert \Phi \vdash g:A \to B \quad \Gamma, a:1 \to A \vert \Phi \vdash \mathrm{comp}_{1, A, B}(a, f) =_{1 \to B} \mathrm{comp}_{1, A, B}(a, g) \; \mathrm{true}}{\Gamma \vert \Phi \vdash f =_{A \to B} g \; \mathrm{true}}$$ This implies that the terminal set $1$ only has one element, the identity function on $1$. ### Empty set There is a specified set $\emptyset$ called the [[empty set]]. $$\frac{\Gamma \vert \Phi \; \mathrm{ctx}}{\Gamma \vert \Phi \vdash \emptyset \; \mathrm{set}}$$ The empty set is characterised by the [[universal property]] that there is a unique function from $\emptyset$ to every set $A$, given by the following rules: $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set}}{\Gamma \vert \Phi \vdash e_A:\emptyset \to A}$$ $$\frac{\Gamma \vert \Phi \vdash A \; \mathrm{set} \quad \Gamma \vert \Phi \vdash a:\emptyset \to A}{\Gamma \vert \Phi \vdash a =_{\emptyset \to A} e_A \; \mathrm{true}}$$ The function $e$ is the function representation of the set $A$ itself. ### Product sets ... ## References * [[Tom Leinster]], _Rethinking set theory_ [arXiv](http://arxiv.org/abs/1212.6543). category: redirected to nlab