Do there exist models of type theory that allow types to contain an uncountable number of inhabitants? Traditionally type theory seems to be swirled in with computable programs as constructive proofs so types are always countable. I want to know if we go outside computable programs do we get types that have an uncountable number of inhabitants?

  • $\begingroup$ Type theory in general, supports real numbers. i think it can be done $\endgroup$ – Nikos M. Jun 15 '14 at 18:23
  • 2
    $\begingroup$ See my answer in cstheory.stackexchange.com/questions/22447/…, but basicaly: yes, there are models of type theory in which the reals are a type, for instance set theory. $\endgroup$ – Andrej Bauer Jun 15 '14 at 21:30
  • $\begingroup$ I've always tried to avoid thinking of types as sets (though of course I understand the similarity). I like the answer however. Post it if you want me to accept it. $\endgroup$ – Jake Jun 15 '14 at 22:11
  • $\begingroup$ We could also mark this as a duplicate of the other question. I do not know what the policy is, perhaps a moderator does. By the way, type theory always believes that nat -> nat is uncountable, so you don't have to think about sets to "see" uncountability. $\endgroup$ – Andrej Bauer Jun 16 '14 at 6:55
  • $\begingroup$ I guess I thought that "nat -> nat" was the computable functions from natural numbers to natural numbers and was thus countable. As you answered with a link this is probably duplicate; my bad $\endgroup$ – Jake Jun 16 '14 at 13:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.