According to wikipedia, a pure type system:

...is a form of typed lambda calculus that allows an arbitrary number of sorts and dependencies between any of these... Pure type systems may obscure the distinction between types and terms and collapse the type hierarchy.

This sounds an awful lot like material set theory. What are the (main) differences?

  • $\begingroup$ The Wikipedia article is short on details. Have you looked at the nLab article? $\endgroup$ – Zhen Lin Aug 6 '13 at 9:52

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.