[FOM] proof-relevance in number theory

[José Manuel Rodriguez Caballero]

Dear FOM members,
There are infinitely many prime numbers, but also there are infinitely many ways to prove this fact, using algebra, analysis and even abstract topology. My question is: Is there a proof-relevant foundation of mathematics where the distinction between Euclid elementary proof and Euler analytical proof is detected by the theory by mean of some invariant? Of course, there are proof-relevant type theories, but I don’t know if they are fine enough to detect differences between algebra and analysis.
Sincerely yours,
Jose M.