Created: December 23, 2021
Modified: December 23, 2021
Modified: December 23, 2021
type theory
This page is from my personal notes, and has not been specifically reviewed for public consumption. It might be incomplete, wrong, outdated, or stupid. Caveat lector.- Inspired by Kevin Buzzard's overview of the state of automatic theorem provers.
- Type theory is like set theory in that sets and types are both 'bags of elements'. But they have different rules.
- In set theory, 'everything is a set', but in type theory, not everything is a type. The elements of a type, its terms, can be arbitrary objects; they do not have to be types (though of course they can be).
- 'Types don't mix'. Two different types have disjoint terms. Unlike sets, there is never any overlap.
- This means that every term in type theory is a member of exactly one type.