Please forgive any unorthodox notation or obvious errors here… I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the simply typed world. In an ML-like language we can encode existential types in terms of universal types:
$\exists a.T(a) \equiv \forall x.(\forall a.T(a) \rightarrow x) \rightarrow x$
Similarly, we could also define sum types in terms of universal types and product types:
$ a + b \equiv \forall x.(a \rightarrow x)\times(b \rightarrow x) \rightarrow x $
This correspondence makes sense to me, since existential types are like infinite sums and universal types are like infinite products.
In a dependently typed language, would it also be possible to define dependent sums in terms of dependent products? This seems close:
$\Sigma(b:B).T(b) \equiv \forall x.(\Pi(b:B).T(b) \rightarrow x) \rightarrow x$
$(a,t) : \Sigma(b:B).T(b) \equiv \lambda f. f\ a\ t$
$\text{fst}\ p \equiv p_B\ (\lambda(b:B).\lambda(\_:T(b)).b)$
$\text{snd}\ p \equiv p_{T (\text{fst}\ p)}\ (\lambda(b:B).\lambda(t:T(b)).t)$
However, I can't convince myself that the definition for snd is well-typed because I can't show that $t : T (\text{fst}\ p)$. Is there some way to make this work?
Best Answer
My understanding is that dependent elimination cannot be derived from impredicative encodings, but I cannot find a reference other than a passing mention in The Implict Calculus of Constructions.