this article is not an exhaustive categorization. What follows is an introduction for those unfamiliar with type theory, covering some of the major approaches. Basics Terms and types In type theory, every term has a type. A term and its type are often written together as "term : type". A common type to include in a type theory is the Natural numbers, often written as "" or "nat". Another is Boolean logic values. So, some very simple terms with their types are: 1 : nat 42 : nat true : bool Terms can be built out of other terms using function calls. In type theory, a function call is called "function application". Function application takes a term of a given type and results in a term of another given type. Function application is written "function argument argument ...", instead of the conventional "function(argument,argument, ...)". For natural numbers, it is possible to define a function called "add" that takes two natural numbers. Thus, some more terms with their types are: add 0 0 : nat add 2 3 : nat add 1 (add 1 (add 1 0)) : nat In the last term, parentheses were added to indicate the order of operations. Technically, most type theories require the parentheses to be present for every operation, but, in practice, they are not written and authors assume readers can use precedence and associativity to know where they are. For similar ease, it is a common notation to write "" instead of "add ". So, the above terms might be rewritten as: 0 + 0 : nat 2 + 3 : nat 1 + (1 + (1 + 0)) : nat Terms may also contain variables. Variables always have a type. So, assuming "x" and "y" are variables of type "nat", the following are also valid terms: x : nat x + 2 : nat x + (x + y) : nat There are more types than "nat" and "bool". We have already seen the term "add", which is not a "nat", but a function that, when applied to two "nat"s, computes to a "nat". The type of "add" will be covered later. First, we need to describe "computes to". Computation Type theory has a built-in notation of computation. The following terms are all different: 1 + 4 : nat 3 + 2 : nat 0 + 5 : nat but they all compute