Although the rules we listed so far allows us to construct everything we need directly, we would still like to be able to use named constants, such as , as a matter of convenience. Informally, we can think of these constants simply as abbreviations, but the situation is a bit subtler in the formalization.
For example, consider function composition, which takes and to . Somewhat unexpectedly, to make this work formally, must take as arguments not only and , but also their types , , :
From a practical perspective, we do not want to annotate each application of with , and , as the are usually quite easily guessed from surrounding information. We would like to simply write . Then, strictly speaking, is not an abbreviation for , because it involves additional implicit arguments which we want to suppress.
Inference of implicit arguments, typical ambiguity (§1.3 (http://planetmath.org/13universesandfamilies)), ensuring that symbols are only defined once, etc., are collectively called elaboration. Elaboration must take place prior to checking a derivation, and is thus not usually presented as part of the core type theory. However, it is essentially impossible to use any implementation of type theory which does not perform elaboration; see [Coq, norell2007towards] for further discussion.