Can we convert existential sentences into functions? I am trying to grasp the basic ideas of type theory. I understand that universally quantified propositions can be considered as functions, which maps terms to "proof objects". Hence a proposition
$$\forall x \;\varphi(x)$$
can be considered as a function which maps a term $u$ to a "proof object" with type $\varphi(u/x)$. Can we do similar things on existential propositions? For example, we add a global function $\tau$ which maps each "proof object" for an existential proposition $\exists x \;\varphi(x)$ to a term, and another global function $\rho$ which maps terms of the form $u = \tau\left(\exists x \;\varphi(x)\right)$ to "proof objects" of type $\varphi(u/x)$.
 A: Let's use untyped $\lambda$-calculus to define functions and rewrite Andreas Blass's ideas.
Notice that what you call "term" and "proof object" are both $\lambda$-terms and that $\forall x \phi(x)$ is the type of all the $\lambda$-terms (or functions) that map $u$ to a proof of $\phi(u)$.
$\exists x \phi(x)$ is the type of a pair $(u,h)$, which may not be unique, where the $\lambda$-term $h$ has $\phi(u)$ as type ($h$ is a "proof" of $\phi(u)$). This pair is the following $\lambda$-term :
$$
\lambda f. f u h
$$
We can define $\lambda$-terms $\tau$ and $\rho$ (projection functions) which respectively return $u$ and $h$ from a pair $p$ :
$$
\tau :=
\lambda p. p(\lambda a.\lambda b. a)
$$$$
\rho :=
\lambda p. p(\lambda a.\lambda b. b)
$$
We can apply those projection functions to our pair and $\beta$-reduce to verify :
$$
\tau (\lambda f. f u h)
=
(\lambda p. p(\lambda a.\lambda b. a))
(\lambda f. f u h)
$$$$
\rightarrow_\beta
(\lambda f. f u h)
(\lambda a.\lambda b. a)
$$$$
\rightarrow_\beta
(\lambda a.\lambda b. a) u h
$$$$
\rightarrow_\beta
u
$$
And
$$
\rho (\lambda f. f u h)
=
(\lambda p. p(\lambda a.\lambda b. b))
(\lambda f. f u h)
$$$$
\rightarrow_\beta
(\lambda f. f u h)
(\lambda a.\lambda b. b)
$$$$
\rightarrow_\beta
(\lambda a.\lambda b. b) u h
$$$$
\rightarrow_\beta
h
$$
So $\tau$ and $\rho$ allow us to retrieve $u$ and the proof of $\phi(u)$ from a proof of $\exists x \phi(x)$.
