# nLab topos of types

### Context

#### Topos Theory

Could not include topos theory - contents

# Contents

## 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) := 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).

## 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, pdf, to appear in Annals of Pure and Applied Logic

Revised on July 24, 2012 04:01:55 by Zoran Škoda (190.26.78.124)