I appreciate your comment but I think you're overcomplicating it for yourself. (And btw I doubt I know more about this than you.)

You say:
"It isn’t clear to me why the encoding of the natural numbers would come up. I would have thought that some statement about the natural numbers would involve some type, considered as the type of natural numbers, which I suppose if you construct it from other simpler primitives would have some kind of encoding."

OK, so let's say we have an agreement, that your representation for the type of natural numbers is practically - from a typing viewpoint - identical to my representation for the type of natural numbers. So then we don't have to worry about the encoding. And it makes sense to do this for all the primitive types we are using.

But then consider your proposition "for all x:X, there exists y:Y, such that P(x,y)". This proposition is itself a type, which is constructed from primitive types. So why would you here, all of sudden, want to distinguish between different proofs, or rather, representations of this particular type?

I think, if we both accept proposition-as-types paradigm, then I am reasoning backwards from it. If the structure of two different proofs of the same (propositional) type matters (whatever the reason), not just existence of these proofs, why shouldn't it matter with the primitive types? It implies that we need to come to an agreement what primitive types we are using, because their structure might matter, too.

And that's why I said - you effectively want your "universal proof equivalence" to be the beta-equivalence of underlying lambda terms, because lambda calculus is a mechanism how we construct the complex types from primitive ones (not all constructions are valid though, there are typing constraints). But, as I already explained, it doesn't really give you a grounding, because there are multiple ways to define primitives in lambda calculus which cause the terms not to be beta-equivalent. So you have to care about having such agreement how you implement these primitives. Hopefully this clears up where it comes from.

But having that agreement in itself then limits what you can prove (in particular, you cannot prove equivalence of different representations, since you're already taking it as an axiom), so you don't really want to have such an agreement. That's why I believe the only sensible way out is to propagate the proof indifference "upwards" - even for complicated types (practically usable propositions), the actual representation shouldn't matter.

No worries, though. If you want the representation to matter, you would do the same thing you do in lambda calculus - you choose some encoding of lambda terms, and take an interpreter for this encoding which implements beta-reduction. When interpreting an encoded lambda term, you can discern different implementations (for example, their complexity properties) of otherwise beta-equivalent lambda terms. Mathematically, this gives a different theory. (Also note there is no reason for your encoding to be working with just lambda abstraction and application as primitives, you can encode different lambda terms in different ways, if you need to. That's what combinatory logic does, it lets you use an arbitrary basis of primitives.)