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.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.