Definition 1.2.2 (Typability relation). We define the typability relation $⊩\subseteq C\times {\mathrm{\Lambda }}_{\mathrm{\Pi }}\times \mathrm{\Pi }$ via:

• (1)
  For every context $\mathrm{\Gamma }$, and variable $x$ not occurring in $\mathrm{\Gamma }$, and type $\tau$, we have $\mathrm{\Gamma },x:\tau ⊩x:\tau$.
• (2)
  Let $\mathrm{\Gamma }$ be a context, $x$ a variable not occurring in $\mathrm{\Gamma }$, and let $\sigma ,\tau \in \mathrm{\Pi }$ be types, and $M$ be a $\lambda$-term. If $\mathrm{\Gamma },x:\sigma ⊩M:\tau$, then $\mathrm{\Gamma }⊩(\lambda x:\sigma .M):(\sigma \to \tau )$.
• (3)
  Let $\mathrm{\Gamma }$ be a context, $\sigma ,\tau \in \mathrm{\Pi }$ be types, and $M,N\in {\mathrm{\Lambda }}_{\mathrm{\Pi }}$ be terms. If $\mathrm{\Gamma }⊩M:(\sigma \to \tau )$ and $\mathrm{\Gamma }⊩N:\sigma$, then $\mathrm{\Gamma }⊩(MN):\tau$.