Inductive types and exact completion

Using the theory of exact completions, I construct a certain class of pretoposes, consisting of what one might call “predicative realizability toposes”, that can act as categorical models of certain predicative type theories, including Martin-Löf Type Theory.