For some motivation I have been wondering about generalizing the topos of coalgebras theorem to relative monads in my previous question. This brought me to wonder about topos objects.

NLab on specifying fully formal ETCS states the following:

For example, the theory of strict toposes is a finite limit theory (it is finitary-algebraic over the category of directed graphs), meaning the notion of strict topos object can be internalized within any finitely complete category.

I am looking for proofs (potentially references) that the theory of strict toposes is indeed a finite limit theory. Or equivalently for the 2 claims, that it is finitary-algebraic over directed graphs and that being finitary algebraic over directed graphs is enough to be finite limit.


1 Answer 1


The original reference for the essential algebraicity of elementary toposes is Freyd's Aspects of topoi (in which the notion of essentially algebraic theory, which is equivalent to that of a finite limit theory, was introduced). Freyd shows that being cartesian closed, and having finite limits are essentially algebraic in §1, and that additionally having a subobject classifier is essentially algebraic in §2.

For an alternative approach based on monadicity, Dubuc and Kelly prove in A Presentation of Topoi as Algebraic Relative to Categories or Graphs (cf. also MacDonald and Stone's Topoi over graphs) that the category of toposes is finitarily monadic over the category of graphs. Since the category of graphs is locally finitely presentable (in fact, a presheaf category), the category of algebras for any finitary monad on it is also locally finitely presentable, hence is the category of models for a finite limit theory: these results may be found in Adámek and Rosický's Locally Presentable and Accessible Categories (cf. the nLab article on locally presentable categories).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.