===== Function type =====
==== Type ====
| @#55CCEE:  context | @#55CCEE:  $X, Y$ ... type |
| @#55CCEE:  context | @#55CCEE:  $\Gamma$ ... context |
| @#FF8866:  rule | @#FF8866:  ${\large\frac{\Gamma,\,x\ :\ X\ \vdash\ y\ :\ Y}{\Gamma\ \vdash\ \lambda x.\,y\ :\ X\to Y}}$ (lambda abstraction) |
| @#FF8866:  rule | @#FF8866:  ${\large\frac{\Gamma\ \vdash\ f\ :\ X\to Y\hspace{1cm}\Gamma\ \vdash\ x\ :\ X}{\Gamma\ \vdash\ f\,x\ :\  Y}}$ (function application) |

==== Discussion ====
Parse ${\large\frac{\Gamma,\,x\ :\ X\ \vdash\ y\ :\ Y}{\Gamma\ \vdash\ \lambda x.\,y\ :\ X\to Y}}$ as ${\large\frac{(\Gamma,\,(x\ :\ X))\ \vdash\ (y\ :\ Y)}{\Gamma\ \vdash\ ((\lambda x.\,y)\ :\ (X\to Y))}}$.

Note that from the wikis perspective, the described type theory is an object language and in it, the context $\Gamma$ is a list of judgements, alla '$a:A$'. That's not to be confused with the context of the meta language (blue boxes) where we also use the notations '$a$...$A$' or '$a\in A$'.

==== Parents ====
=== Element of ===
[[Type]]