The type is written "" or "" and the single canonical term is written "*". The unit type is used to show that something exists or is computable. If for a type "A", you can create a function of type " A", you know that "A" has one or more terms. When a type has at least 1 term, we say it is "inhabited". Boolean type The Boolean type has exactly 2 canonical terms. The type is usually written "bool" or "" or "". The canonical terms are usually "true" and "false". The Boolean type is defined with an eliminator function "if" such that: if true b c b if false b c c Product type The product type has terms that are ordered pairs. For types "A" and "B", the product type is written "A B". Canonical terms are created by the constructor function "pair". The terms are "pair a b", where "a" is a term of type "A" and "b" is a term of type "B". The product type is defined with eliminator functions "first" and "second" such that: first (pair a b) a second (pair a b) b Besides ordered pairs, this type is used for the logical operator "and", because it holds an "A" and a "B". It is also used for intersection, because it holds one of both types. If a type theory has dependent typing, it has dependent pairs. In a dependent pair, the second type depends on the value of the first term. Thus, the type is written " a:A . B(a)" where "B" has type "A U". It is useful when showing existence of an "a" with property "B(a)". Sum type The sum type is a "tagged union". That is, for types "A" and "B", the type "A + B" holds either a term of type "A" or a term of type "B" and it knows which one it holds. The type comes with the constructors "injectionLeft" and "injectionRight". The call "injectionLeft a" takes "a : A" and returns a canonical term of type "A + B". Similarly, injectionRight b" takes "b : B" and returns a canonical term of type "A + B". The type is defined with an eliminator function "match" such that for a type "C" and functions "f : A C" and "g : B C": match (injectionLeft a) C f g (f a) match (injectionRight b) C