Every theory is eventually of presheaf type

Christian Espíndola, Kristóf Kanalas

We give a detailed and self-contained introduction to the theory of λ-toposes and prove the following: 1) A λ-separable λ-topos has enough λ-points. 2) The classifying λ-topos of a κ-site (C,E) is a presheaf topos (assuming κ ⊲ λ =λ ^< λ, |C|, |E| < λ).

Keywords: κ-topos, theory of presheaf type

2020 MSC: 18F10, 03G30

Theory and Applications of Categories, Vol. 44, 2025, No. 12, pp 344-371.

Published 2025-05-06.

http://www.tac.mta.ca/tac/volumes/44/12/44-12.pdf

TAC Home