A.2.11 Definitions

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 f:Aβ†’B and g:Bβ†’C to g∘f:Aβ†’C. Somewhat unexpectedly, to make this work formally, ∘ must take as arguments not only f and g, but also their types A, B, C:


From a practical perspective, we do not want to annotate each application of ∘ with A, B and C, as the are usually quite easily guessed from surrounding information. We would like to simply write g∘f. Then, strictly speaking, g∘f is not an abbreviation for λ(x:A).g(f(x)), 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 theoryPlanetmathPlanetmath. However, it is essentially impossible to use any implementation of type theory which does not perform elaboration; see [Coq, norell2007towards] for further discussion.

Title A.2.11 Definitions