I added the definitions. Rereading your question, I see you were looking at sets of reals, while my answer addresses subsets of $\omega$. But perhaps weakly finite dilators are a $\Pi^1_2$-complete set of reals?

One more thing: I think the translation of set theory into type theory is actually due to Peter Aczel in the context of CZF and predicative type theory, but Benjamin Werner studied it in the context of IZF and Coq, and he also formalized it in Coq.

I mean, Agda is predicative in not giving power sets. Of course, it goes beyond “predicative mathematics” in its use of inductive (and inductive-inductive, etc.) types. So I mean it is “generalized predicative”, giving strength via controlled means, as Andrej said, but without power sets.

Pointing to Coq seems slightly inappropriate in connection with this question, as Coq in effect allows the formation of power sets via the impredicative sort Prop. With Benjamin Werner's embedding of set theory into type theory, the power set axiom is provable. In fact, Coq is proof-theoretically a bit stronger than ZFC. Agda however, is fully predicative.

Speaking of Feferman, he just but up these old, but previously unpublished notes on Predicative Foundations of Analysis: math.stanford.edu/~feferman/papers/pfa(1).pdf They substantiate in more detail his claims (building on work of Weyl) on how most of classical analysis and substantial portions of modern analysis can be developed on the basis of a system conservative over Peano Arithmetic.

Can you add the tag lo.logic ? Thanks! (Later on, there will perhaps be a need for a HoTT tag, but in the meantime I think adding logic as a tag to questions like this will help, as the people interested in HoTT aren't necessarily interested in set theory, nor abstract homotopy or infinity-topos theory outside of the type-theoretic context.)

Check out the topos approaches to quantum mechanics, as initiated by Isham/Butterfield and Döring/Isham (the contravariant approach, see review by Flori: arxiv.org/abs/1106.5660). There's also a covariant approach, developed by Heunen, Landsman and Spitters (see Wolters' comparison of the approaches: arxiv.org/abs/1010.2031). That should get you started.

@Andrej: yes, you make sense, and I guess my objection is more terminological: I would take first-order PA to satisfy an induction schema for first-order formulas only, whereas the version here (in Lambek and Scott) is schematic in all (ambiently definable) predicates on N. If you have a PA object N in a topos that only satisfies induction for first-order formulas, then it could be non-standard, but in the topos logic you could then separate out the standard part and make a NNO.

Andrej, aren't these results about higher-order type theories with power types and full comprehension? They say that a topos with NNO is equivalent to a model of higher-order type theory with full comprehension, in the sense that you can go back and forth (using internal language and syntactic category). Since full comprehension is always assumed, this says little about first-order PA.

Of course you're right that normalization by evaluation only produces normal forms for a congruence relation. For these eta-like rules you have to be careful I you want to extract a normalizing reduction relation, which is why normalization by evaluation seems preferable in this case. I've edited my answer to reflect this, and added another reference you might find helpful.