Kleene computable functionals and the higher order existence property
Andre Scedrov · Journal of Pure and Applied Algebra · 1988
Let F be the free topos with the natural number object (n.n.o.). Let C be the full Cartesian closed subcategory of F generated by n.n.o. We show that the morphisms of C are given by the Kleene computable functionals that are provably total in intuitionistic type theory. We thus establish the existence property for functionals of finite type.