[[!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}$$ * Membership judgments: $$\Gamma \vdash a \in A$$ * 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 membership judgments: $$\frac{}{() \; \mathrm{setctx}} \qquad \frac{\Gamma \; \mathrm{setctx} \quad \Gamma \vdash A \; \mathrm{set}}{(\Gamma, a \in A) \; \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{true}}{\Gamma \vert (\Phi, A \; \mathrm{true}) \; \mathrm{ctx}}$$ Equality in ETCS is a proposition, and is formed by the [[predicate]] ## 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