# 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 $\mathrm{\pi \x9d\x97\x82\pi \x9d\x97\x8c\pi \x9d\x96\u038e\pi \x9d\x97\x8a\pi \x9d\x97\x8e\pi \x9d\x97\x82\pi \x9d\x97\x8f}$, 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\beta \x86\x92B$ and $g:B\beta \x86\x92C$ to $g\beta \x88\x98f:A\beta \x86\x92C$. Somewhat unexpectedly, to make this work formally, $\beta \x88\x98$ must take as arguments not only $f$ and $g$, but also their types $A$, $B$, $C$:

$$\beta \x88\x98:\beta \x89\u2018\mathrm{\Xi \xbb}(A:{\mathrm{\pi \x9d\x92\xb0}}_{i}).\mathrm{\Xi \xbb}(B:{\mathrm{\pi \x9d\x92\xb0}}_{i}).\mathrm{\Xi \xbb}(C:{\mathrm{\pi \x9d\x92\xb0}}_{i}).\mathrm{\Xi \xbb}(g:B\beta \x86\x92C).\mathrm{\Xi \xbb}(f:A\beta \x86\x92B).\mathrm{\Xi \xbb}(x:A).g(f(x)).$$ |

From a practical perspective, we do not want to annotate each application of $\beta \x88\x98$ with $A$, $B$ and $C$, as the are usually quite easily guessed from surrounding information. We would like to simply write $g\beta \x88\x98f$. Then, strictly speaking, $g\beta \x88\x98f$ is not an abbreviation for $\mathrm{\Xi \xbb}(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 theory^{}. 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 |
---|---|

\metatable |