nLab
effective topos

The effective topos is an example of an elementary topos with a natural numbers object which is not a Grothendieck topos. 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 $\mathrm{Hom}(1,-)$ from the effective topos into $\mathrm{Set}$ 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.

Reference

• 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.