nLab topos of types



Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




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

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

T(C)Sh J p(τC). \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.


In terms of the coherent hyperdoctrine

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

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

T(C)Sh(𝒮 C δ). \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

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

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

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

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

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

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

This is (Coumans, theorem 39).


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

Last revised on May 6, 2016 at 20:34:13. See the history of this page for a list of all contributions to it.