nLab topos of types

Definition

Let $C$ be a coherent category. Write $\tau C$ for the category whose objects are pairs $(X,F)$ where $X$ is an object of $C$ and $F$ is a prime filter on $Sub_C(X)$. This is the full subcategory of the category of filters of $C$ spanned by the prime filters. Jet $J_p$ be the Grothendieck topology on $\tau C$ induced from the coherent topology on the category of filters.

As defined by Makkai, the topos of types $\mathbf{T}(C)$ of $C$ is the sheaf topos

$$\mathbf{T}(C) \coloneqq Sh_{J_p}(\tau C) \,.$$

Note: The word “types” here has nothing to do with type theory. Instead, refers to the notion of type in model theory.

Properties

In terms of the coherent hyperdoctrine

Let $C$ be a coherent category. The canonical extension $\mathcal{S}_C^\delta$ of its coherent hyperdoctrine $\mathcal{S}_C$ is naturally an internal locale in the presheaf topos $[C^{op}, Set]$ (as well as in the sheaf topos $Sh_{coh}(C)$ for the coherent topology on $C$).

The topos of types is equivalent to the topos of internal sheaves over this internal locale.

$$\mathbf{T}(C) \simeq Sh(\mathcal{S}_C^\delta) \,.$$

This is due to (Coumans, theorem 25).

In particular this implies that there is a localic geometric morphism

$$\mathbf{T}(C) \to Sh_{coh}(C) \,.$$

Let $Mod(C) \simeq Func_{coh}(C,Set)$ be the category of models of the coherent theory given by $C$ in Set.

There is a full subcategory $\mathcal{K} \hookrightarrow Mod(C)$ such that the Yoneda extension of the evaluation map $ev : C \to Func(\mathcal{K}, Set)$ is the inverse image of a geometric morphism

$$\phi_{ev} : Set^{\mathcal{K}} \to Sh_{coh}(C) \,.$$

The hyperconnected / localic factorization of this morphism is through the topos of types of $C$:

$$\phi_{ev} : Set^{\mathcal{K}} \stackrel{hyperconn.}{\to} \mathbf{T}(C) \stackrel{localic}{\to} Sh_{coh}(C) \,.$$

This is (Coumans, theorem 39).

Related concepts

• canonical extension

References

The notion was introduced in

• Michael Makkai, The topos of types, Logic Year 1979-80 (Proc. Seminars and Conf. Math. Logic, Univ. Connecticut, Storrs, Conn., 1979/80), Lecture Notes in Math. 859, Springer, Berlin (1981) pp. 157-201, doi.

The relation to canonical extension is made explicit in

• Dion Coumans, Generalizing canonical extensions to the categorical setting, Annals of Pure and Applied Logic December 2012, Vol.163(12):1940–1961 doi:10.1016/j.apal.2012.07.002, pdf