## Idea ## ## Definition ## Let $A,B$ be two types. We introduce a type $A \to B$ called the **function type**. The constructors for this type are written as $$(\lambda x . y) : A \to B$$ where $x:A$ and $y:B$. These can be computed (on application) using $\beta$-reduction: $$(\lambda x. y)z \equiv y[x/z]$$ which says take $y$ and replace all occurrences of $x$ with $z$. ## Properties ## ## References ## * [[HoTT book]] category: type theory