natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
The theory of objects is the logical theory whose models in a category $\mathcal{C}$ are precisely the objects of $\mathcal{C}$. From an algebraic perspective one can think of it as the theory of an algebra with no operations.
The theory of objects $\mathbb{O}$ is the theory with no axioms over the signature with a single type and no primitive symbols except equality.
Of course, $\mathbb{O}$ is a geometric theory, and as models for $\mathbb{O}$ in a topos $\mathcal{E}$ correspond to objects of $\mathcal{E}$, we can use its classifying topos to get a representation of the objects of $\mathcal{E}$.
The classifying topos for the theory of objects is the presheaf topos $[FinSet, Set]$ over the opposite category of the category FinSet of finite sets.
This follows from the fact that $\mathbb{O}$ is the algebraic theory of a 1-sorted algebra without operations whence its algebras are merely sets. The classifying topos for algebraic theories is quite generally given by the presheaf topos on the opposite of the category of finitely presentable models in our case just the finite sets.
For a direct proof see at classifying topos for the theory of objects. For base toposes $\mathcal{S}$ other than $Set$, it is a theorem due to Andreas Blass that the theory of objects has a classifying topos precisely if $\mathcal{S}$ has a natural numbers object (Blass 1989).
In the syntax-free approach to geometric theories of Johnstone (2002, I B4.2) the theory of objects corresponds to the forgetful functor sending an $\mathcal{S}$-topos to its underlying category. (See at geometric theory the section on the functorial definition.)
When viewed as algebraic theory the initial algebra (in $Set$) is the empty set which satisfies $(\exists x)\top\vdash\bot$. Adding the sequent to the theory of objects one obtains the theory of empty objects $\mathbb{O}_\emptyset$, its models are the initial objects. Its classifying topos is $Set$ with $\emptyset$ as generic object. Whence the duality between quotient theories and subtoposes implies that $Set[\mathbb{O}]$ contains $Set[\mathbb{O}_\emptyset]$. The pattern that the classifying topos of an algebraic theory contains a copy of $Set$ as a subtopos classifying $Th(\mathfrak{A}_0)$ i.e. the theory of all geometric sequents holding at the initial algebra $\mathfrak{A}_0$ in Set is valid more generally (see at geometric type theory for another example).
If instead of an additional axiom one adds a single constant symbol to the signature of $\mathbb{O}$ one obtains the theory of pointed objects $\mathbb{O}_\ast$ i.e. the empty theory relative to the signature with a single sort and a single constant. Its models are pointed objects and its classifying topos is $[FinSet_\ast,Set]$. (See the discussion&references at classifying topos for the theory of objects.)
The theory of morphisms $\mathbb{O}^2$ is the theory with no sequents over the signature with two sort symbols $O^0$, $O^1$ and a function symbol $f_O:O^0\to O^1$. It is the theory of $\mathbb{O}$-model homomorphisms and its models in a Grothendieck topos $\mathcal{E}$ are the morphisms of $\mathcal{E}$. It is the dual theory of the theory classified by the Sierpinski topos $Set^2$, or in other words, its classifying topos is $Set[\mathbb{O}^2]=Set[\mathbb{O}]^{Set^2}$.
Sections B4.2, D3.2 of
For the equivalence of having an NNO to having a classifier for objects:
cf. Johnstone (2002 II, p.773) and Joyal-Tierney (1984). For some further information on $FinSet_\exists$ see the references at generic interval. ↩
Last revised on October 27, 2022 at 10:50:15. See the history of this page for a list of all contributions to it.