A lot of mathematics is based on sets, whereas sets and types are not formally the same thing. Some mathematicians are trying to formulate a basis for mathemat

A lot of mathematics is based on sets, whereas sets and types are not formally the same thing. Some mathematicians are trying to formulate a basis for mathematics in type theory. For example, there is the Univalent Foundations of mathematics proposed by Vladimir Veovodsky. This reduces logic, set theory, category theory (actually groupoids) and higher abstractions to homotopy theory (well, certain explicit constructions in such anyway) which is then modelled in Martin-Löf type theory. By the Curry-Howard isomorphism there is a correspondence between types and proofs (specifically types in the simply typed lambda calculus and proofs in the intuitionistic logic or if you add dependent types, then also predicate logic). The real difference is that functions in type theory are computable, whereas functions in mathematics (based on sets) need not be.