[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] ## ETCS We present William Lawvere's Elementary Theory of the Category of Sets as [[first order logic]] over [[type theory]]. 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 \vdash A \; \mathrm{prop}}{\Gamma \vert (\Phi, A \; \mathrm{true}) \; \mathrm{ctx}}$$ 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}}$$ and the [[existential quantifier]]: $$\frac{\Gamma, x:A \to B \vdash P \; \mathrm{prop}}{\Gamma \vdash \exists x:A \to B.P \; \mathrm{prop}}$$ $$\frac{\Gamma \vdash f:A \to B \quad \Gamma, x:A \to B \vdash P \; \mathrm{prop} \quad \Gamma \vdash P[f/x] \; \mathrm{true}}{\Gamma \vdash \exists x:A \to B.P \; \mathrm{true}}$$ 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}$$ The [[equality]] in ETCS is a homogeneous binary relation, and is formed by the following rule: $$\frac{\Gamma \vdash f:A \to B \quad \Gamma \vdash g:A \to B}{\Gamma \vdash f =_{A \to B} g \; \mathrm{prop}}$$ Equality also satisfies reflexivity, symmetry, and transitivity, making it into a equivalence relation $$\frac{\Gamma \vdash f:A \to B}{\Gamma \vdash f =_{A \to B} f \; \mathrm{true}}$$ $$\frac{\Gamma \vdash f:A \to B \quad \Gamma \vdash g:A \to B}{\Gamma \vdash (f =_{A \to B} g) \implies (g =_{A \to B} f) \; \mathrm{true}}$$ $$\frac{\Gamma \vdash f:A \to B \quad \Gamma \vdash g:A \to B \quad \Gamma \vdash h:A \to B}{\Gamma \vdash ((f =_{A \to B} g) \wedge (g =_{A \to B} h)) \implies (f =_{A \to B} h) \; \mathrm{true}}$$ ## ETCG The elementary theory of the (2, 1)-category of (constructive) groupoids. We work in first order logic over type theory, consisting of three layers, a layer of (constructive) groupoids, a layer of (constructive) sets, and a layer of (constructive) propositions. The judgments are as follows: $$\Gamma \vdash A \; \mathrm{grpd}$$ $$\Gamma \vdash a:A$$ $$\Gamma \vert \Xi \vdash A \; \mathrm{set}$$ $$\Gamma \vert \Xi \vdash a \in A$$ $$\Gamma \vert \Xi \vert \Phi \vdash A \; \mathrm{prop}$$ ... category: redirected to nlab