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?