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.
