It is an environment for higher orderrecursion 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, -)$ from the effective topos into Set, the inverse image part of a geometric morphism $Set \to Eff$ preserves the natural numbers object, giving a suitable version of this result in the external logic as well).

The effective topos construction alluded in the above paragraph can be performed more generally, in every topos $E$ with a natural numbers object, replacing Set. To every such topos one constructs the corresponding “external” effective topos $e E$ and the correspondence $E \mapsto e E$ extends to a functor admitting a fully faithfulright 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).

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.