That is, the type of the "if" term is either the type of the second or third argument, depending on the value of the first argument. In actuality, "if a B C" isn't defined using "if", but that gets into details too complicated for this introduction. Because the type can contain computation, dependent typing is amazingly powerful. When mathematicians say "there exists a number such that is prime" or "there exists a number such that property holds", it can be expressed as a dependent type. That is, the property is proven for the specific "" and that is visible in the type of the result. There are many details to dependent typing. They are too long and complicated for this introduction. See the article on dependent typing and the lambda cube for more information. Universes Π-terms return a type. So what is the type of their return value? Well, there must be a type that contains types. A type that contains other types is called a "universe". It is often written with the symbol . Sometimes there is a hierarchy of universes, with " : ", " : ", etc.. If a universe contains itself, it can lead to paradoxes like Girard's Paradox. For example: Common "by rule" types and terms Type theories are defined by their rules of inference. There are rules for a "functional core", described above, and rules that create types and terms. Below is a non-exhaustive list of common types and their associated terms. The list ends with "inductive types", which is a powerful technique that is able to construct all the other ones in the list. The mathematical foundations used by the proof assistants "Coq" and "Lean" are based on the "Calculus for Inductive Constructions" which is the "Calculus of Constructions" (its "functional core") with inductive types. Empty type The empty type has no terms. The type is usually written "" or "". It is used to show that something is uncomputable. If for a type "A", you can create a function of type "A ", you know that "A" has no terms. An example for the type "A" might be "there exists a number such that both is even and is odd". (See "Product Type" below for how the example "A" is constructed.) When a type has no terms, we say it is "uninhabited". Unit type The unit type has exactly 1 canonical term.