# Axioms of a Local Set Theory

So this one’s from J.L. Bell’s Toposes and Local Set Theories. Taking a look at the axioms, I’m struggling to see why any sequent of the form$$\emptyset$$:t would be of much use... Take the axiom of “Unity” for example... what good does it do to have “the set of all$$\emptyset$$ such that x of type 1 equals a term of type 1” as an axiom? If the set of all$$\emptyset$$ is empty, then how is a supposedly “empty” set displaying “qualities” in such a sense? What am I missing here?

• @SCappella yes empty set – mizejonathan17 2 days ago

The axiom of unity is saying that all terms of type $$\mathbf 1$$ are equal to the canonical term of type $$\mathbf 1$$, that is, $$*$$. And this is true without any assumptions. (A more modern treatment would probably put $$x_{\mathbf 1}$$ as a premise: $$x: \mathbf 1 \vdash x = *$$).
The axioms of products say that the $$i$$th projection of a tuple is the $$i$$th term of the tuple, and that any element in a product is equal to the tuple of its projections. (Again, most treatments I've seen would put variables in the premises). Other than the variables, no premises are needed.