Type theory. The Curry-Howard-Lambek correspondence shows that type theory, logic, and category theory are equivalent. Even ideas such as set theory can be gr

Type theory. The Curry-Howard-Lambek correspondence shows that type theory, logic, and category theory are equivalent. Even ideas such as set theory can be grounded in type theory (due to the univalence axiom), as type theory can be used as a foundation (via homotopy type theory) for all of mathematics. There are lots of practical uses. For example, the billion dollar mistake [1] is painfully obvious when viewed through the lens of type theory. Software such as Coq can be used to write verified (provably correct) software and can be used by mathematicians for proving theorems. [1] http://lambda-the-ultimate.org/node/3186 http://lambda-the-ultimate.org/node/3186