Identity Function

Definition

In type theory, the identity function on type $A$ is a function of the form,

$$\begin{array}{r}\mathrm{id}:A\to A\\ \mathrm{id}=\lambda x.x\end{array}$$