## 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)a \equiv y[a/x]$$ which says take $y$ and replace all occurrences of $x$ with $a$ for an $a : A$. Given any [[type]] $A$, there is a function called the *identity function* of $A$ denoted and defined by $$id_A : A \to A$$ $$ id_A \equiv \lambda x.x$$ Given any types $A,B,C$ and two functions $f : A \to B$, $g : B \to C$ the composition of $f$ and $g$ is the function $$g \circ f : A \to C$$ $$ (g \circ f) (x) \equiv g(f(x))$$ ## References ## * [[HoTT book]] category: type theory