nLab effective topos

Contents

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Constructivism, Realizability, Computability

Contents

Idea

The effective topos EffEff is an example of an elementary topos with a natural numbers object which is not a Grothendieck topos (and doesn’t even have a geometric morphism to Set).

It is an environment for higher order recursion theory, where, in the internal logic, it is provable that every total function from natural numbers to natural numbers is recursive (furthermore, the functor Hom(1,)Hom(1, -) from the effective topos into Set, the inverse image part of a geometric morphism SetEffSet \to Eff preserves the natural numbers object, giving a suitable version of this result in the external logic as well).

It can be specified as the realizability topos for Kleene's first algebra.

The effective topos construction alluded in the above paragraph can be performed more generally, in every topos EE with a natural numbers object, replacing Set. To every such topos one constructs the corresponding “external” effective topos eEe E and the correspondence EeEE \mapsto e E extends to a functor admitting a fully faithful right adjoint. Kleene’s first algebra can also be replaced by any partial combinatory algebra, or even some more general types of gadgets; toposes obtained in this way are called realizability toposes.

The effective topos is the category obtained from the category of sets by first freely adjoining recursively-indexed coproducts (but being careful to preserve the empty set), and then adding quotients of (pseudo-)equivalence relations. (RobinsonRosolini).

References

Reviews include

  • Stijn Vermeeren, section 3 of Realizability Toposes, 2009 (pdf)

  • J.M.E. Hyland, The effective topos in A. S. Troelstra (ed.) D. van Dalen (ed.) , The L.E.J. Brouwer Centenary Symposium, North-Holland (1982) pp. 165–216.

  • Bart Jacobs, Chapter 6 in: Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, Elsevier (1998) [ISBN:978-0-444-50170-7, pdf]

In the context of triposes:

  • Andy Pitts, The theory of triposes, thesis, pdf

Then

  • Sori Lee, Jaap van Oosten, Basic subtoposes of the effective topos, arxiv/1201.2571

  • Edmund Robinson, Giuseppe Rosolini, Colimit completions and the effective topos, The Journal of symbolic logic, 55, no 2 (1990) (JSTOR)

  • Aurelio Carboni, Some free constructions in realizability and proof theory, J. Pure App. Alg., Vol. 103 Issue 2 (1995), 117-233. (web)

Last revised on January 22, 2023 at 10:39:22. See the history of this page for a list of all contributions to it.