to the term "5 : nat". In type theory, we use the words "reduction" and "reduce" to refer to computation. So, we say "0 + 5 : nat" reduces to "5 : nat". It can be written "0 + 5 : nat 5 : nat". The computation is mechanical, accomplished by rewriting the term's syntax. Terms that contain variables can be reduced too. So the term "x + (1 + 4) : nat" reduces to "x + 5 : nat". (We can reduce any sub-term within a term, thanks to the Church-Rosser theorem.) A term without any variables that cannot be reduced further is a "canonical term". All the terms above reduce to "5 : nat", which is a canonical term. The canonical terms of the natural numbers are: 0 : nat 1 : nat 2 : nat etc. Obviously, terms that compute to the same term are equal. So, assuming "x : nat", the terms "x + (1 + 4) : nat" and "x + (4 + 1) : nat" are equal because they both reduce to "x + 5 : nat". When two terms are equal, they can be substituted for each other. Equality is a complex topic in type theory and there are many kinds of equality. This kind of equality, where two terms compute to the same term, is called "judgemental equality". Functions In type theory, functions are terms. Functions can either be lambda terms or defined "by rule". Lambda terms A lambda term looks like "(λ variablename : type1 . term)" and has type "type1 type2". The type "type1 type2" indicates that the lambda term is a function that takes a parameter of type "type1" and computes to a term of type "type2". The term inside the lambda term must be a value of "type2", assuming the variable has type "type1". An example of a lambda term is this function which doubles its argument: (λ x : nat . (add x x)) : nat nat The variable name is "x" and the variable has type "nat". The term "(add x x)" has type "nat", assuming "x : nat". Thus, the lambda term has type "nat nat", which means if it is given a "nat" as an argument, it will compute to a "nat". Reduction (a.k.a. computation) is defined for lambda terms. When the function is applied (a.k.a. called), the argument is substituted for the parameter.