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?