Using the type of natural numbers $\mathrm{N}$ and the type of propositions $\mathrm{Prop}$, we can make Peano arithmetic in the style of type theory.
https://ncatlab.org/nlab/show/Peano+arithmetic
Since Peano arithmetic is a first-order theory, the range of quantification is limited to $\mathrm{N}$.
If I allow quantification over $\mathrm{Prop}$, is it second-order?
"Second-order" is described as allowing quantification over subsets. However, subsets and propositions are conceptually distinct.
Besides, if this is second-order, I do not know how to make it third-order.