Functions usually get encoded in set theory as follows. A function $A\to B$ is a subset $f\subset A\times B$ such that $\pi_1:f\to A$ is a bijection.
In type theory to give a function $A\to B$ is to write a program computing a term of $B$ given a term of $A$.
But can we simulate the set-theoretic notion of function in type theory? Is this a useful notion? Are there references on this?