is a term (in a context without the free variable) of the dependent product type $\prod_{x\colon A} B$. If $B$ is defined in the context without the free variable, then this expression is a term of the function type$A \to B$ or $B^A$.

Often we make the presence of the free variable explicit in the notation, saying that $t[x]$ is a term of type $B[x]$; then

(2)$\lambda_{x\colon A} t[x] ,$

a term of the dependent product $\prod_{x\colon A} B[x]$. Or if $t[x]$ is a term of the constant type $B$, then the same expression is a term of the function type $A \to B$.