In mathematical logic that I'm used to (i.e. we have first-order formulas and a sequent calculus to derive formula's from axioms), we never prove that the peano axioms are true for the natural numbers, simply because the proof calculus is "at a completely different level" than the structure $(\mathbb N,\sigma,0)$ or $(\mathbb N,+,0,1)$, where $\sigma$ is the successor function.
But in type theory using the curry-howard isomorphism, we treat proofs as "first class citizens" (quote from wikipedia). That is, we define the underlying structures about which we want to talk as types, but the propositions themselves are also types.
That means that both the peano axioms and the $\sigma$ are $\lambda$-functions in the same "program", and therefore could potentially "talk to each other". i.e. the structure $(\mathbb N,\sigma,0)$ is defined in the same language as the peano axioms.
This made me conjecture: Even though we cannot prove that the peano axioms are true for $(\mathbb N, \sigma,0)$ using (formal logic + sequent calculus), could we prove it using (type theory + curry howard isomorphism)?
Is my understanding correct, that in (formal logic + sequent calculus), it is the case that $(\mathbb N, \sigma,0)$ and PA are objects within different universes that cannot talk to eachother, but that in (Type theory + CHI) they are in the same universe and can talk to eachother?
is it correct that we can prove the correctness of the peano axioms from the definition of $(\mathbb N,\sigma,0)$ in (type theory + CHI)? How do we show this?
edit: practically, I'd want to implement this in the Lean theorem prover if possible.