A.2.11 Definitions

Although the rules we listed so far allows us to construct everything we need directly, wewould still like to be able to use named constants, such as $\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}$, as a matter ofconvenience. Informally, we can think of these constants simply asabbreviations, but the situation is a bit subtler in the formalization.

For example, consider function composition, which takes $f:A\to B$ and$g:B\to C$ to $g\circ f:A\to C$. Somewhat unexpectedly, to make this work formally, $\circ$ must take as arguments not only $f$ and $g$, but also their types $A$, $B$, $C$:

$$\circ :\equiv \lambda (A:{𝒰}_i).\lambda (B:{𝒰}_i).\lambda (C:{𝒰}_i).\lambda (g:B\to C).\lambda (f:A\to B).\lambda (x:A).g(f(x)).$$

From a practical perspective, we do not want to annotate each application of$\circ$ with $A$, $B$ and $C$, as the are usually quite easily guessed from surrounding information. We would like to simply write $g\circ f$.Then, strictly speaking, $g\circ f$ is not an abbreviation for $\lambda (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 calledelaboration. Elaboration must take place prior to checking a derivation, and isthus not usually presented as part of the core type theory. However, it isessentially impossible to use any implementation of type theory which does notperform elaboration; see [Coq, norell2007towards] for further discussion.