Schanuel topos



Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




The Schanuel topos (also called the Myhill-Schanuel topos) is the Grothendieck topos of combinatorial functors. It plays an important role in computer science in the theory of name-binding calculi and in William Lawvere‘s approach to petit toposes. It can be viewed as a categorical variant of the Fraenkel-Mostowski model of set theory.


The Schanuel topos is the sheaf topos Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) where FinSet mono opFinSet^{op}_{mono} is the opposite of the category of finite sets and monomorphisms and the coverage is the collection of all sieves generated by singletons {f}.\{f\}\quad.


  • The objects of the Schanuel topos are called nominal sets and correspond precisely to the pullback preserving functors FinSet monoSetFinSet_{mono}\to Set.

  • The Schanuel topos Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is atomic over SetSet (S. Schanuel, cf. (Wraith 1978), p.335) hence Boolean. This fact can be viewed as a reflex of the urelements in Fraenkel-Mostowski set theory.

  • Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is the classifying topos Set[D ]Set[D_\infty] for the theory of infinite decidable objects D D_\infty i.e. for a Grothendieck topos \mathcal{E} geometric morphisms Sh(FinSet mono op,J)\mathcal{E}\to Sh(FinSet^{op}_{mono},J) correspond to infinite decidable objects in \mathcal{E}. Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is equivalent to Sh ¬¬([FinSet mono,Set])Sh_{\neg\neg}([FinSet_mono,Set]).

  • Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is the category of continuous actions for the group of bijections of NN equipped with the topology derived from the product topology for NN.\prod_{N}N\quad .

  • Sh(FinSet mono op,J)Sh(FinSet^{op}_{mono},J) is the Kleisli category of the monad on the topos of species Set FinSet isoSet^{FinSet_{iso}} induced by the inclusion of finite sets and bijections FinSet isoFinSet monoFinSet_{iso}\hookrightarrow FinSet_{mono} (cf. Fiore-Menni 2004).


For some information on the history of the Schanuel topos see section 10 of Menni (2009, pp.529f).


  • M. Fiore, M. Menni, Reflective Kleisli Subcategories of the Category of Eilenberg-Moore Algebras for Factorization Monads , TAC 15 no. 2 (2004) pp.40-65. (pdf)

  • M. J. Gabbay, A. M. Pitts, A new approach to abstract syntax with variable binding, Formal Aspects of Computing 13 (2002) pp.341-363. (draft)

  • Peter Johnstone, Sketches of an Elephant vols. I,II, Oxford UP 2002. (pp.79f, 691, 925)

  • F. William Lawvere, Qualitative Distinctions between some Toposes of Generalized Graphs , Cont. Math. 92 (1989). (pp.298f)

  • S. Mac Lane, I. Moerdijk, Sheaves in Geometry and Logic , Springer Heidelberg 1994. (pp.155, 158)

  • Matías Menni, About N-quantifiers , Appl. Cat. Struc. 11 (2003) pp.421-445. (preprint)

  • Matías Menni, Algebraic categories whose projectives are explicitly free , TAC 22 no.20 (2009) pp.509-541. (abstract)

  • Sam Staton, Name-passing process calculi: operational models and structural operational semantics, Technical Report 688 CL University Cambridge 2007. (pdf)

  • G. Wraith, Intuitionistic Algebra: Some Recent Developments of Topos Theory , Proc. ICM Helsinki (1978) pp.331-337. (pdf)

Last revised on August 5, 2016 at 10:07:44. See the history of this page for a list of all contributions to it.