In Coq, the
nat, the type of natural numbers, has type
Set. By the Curry-Howard Isomorphism, all propositions of type
Prop are types of corresponding proof terms. How do
nats or other instances of
Set figure into this isomorphism?
In other words, is there a correspondent for
Sets in the Curry-Howard isomorphism, as there is for
Props and proof terms, or are they outside the things that have correspondents in the Curry-Howard Isomorphism?
Sorry for the imprecise wording, I'm struggling to express my question clearly, probably because of a poor understanding of the Curry-Howard Isomorphism, happy to be corrected on any misunderstandings I have expressed above.