Reference: Toposes and Theories

Source

Consider a geometric theory, \(\mathbb{T}\). We construct the syntactic category as follows:

• The objects are pairs of a context \(x_1 : X_1 \dots x_n : X_n\) and a formula \(\phi(x_1 \dots x_n)\). Intuitively, this represents the type \(\{\vec{x} \in \prod_{i=1}^n X_i \mid \phi(\vec{x})\}\).

• The morphisms \((\vec{x},\phi) \to (\vec{y},\psi)\) are, not functions, but \(\mathrm{T}\)-provably functional relations. Specifically, they're formulas \(\theta(\vec{x},\vec{y})\) such that the following are provable.

  \[\begin{align*} \phi(\vec{x}) &\vdash \exists \vec{y}, \theta(\vec{x},\vec{y}) \\ \theta(\vec{x},\vec{y}) &\vdash \phi(\vec{x}) \land \psi(\vec{y}) \\ \theta(\vec{x},\vec{y}) \land \theta(\vec{x},\vec{z}) &\vdash \vec{y} = \vec{z} \end{align*}\]

  By using functional relations instead of functions, we work around the need for a unique choice principle.

• Morphisms \(\theta_1\) and \(\theta_2\) are equivalent when \(\theta_1(\vec{x},\vec{y}) \dashv\vdash \theta_2(\vec{x},\vec{y})\).

TODO: Explain the Grothendieck topology. Explain what happens with morphisms.