Example of existence proof in dependent typing?
$\Sigma$-types in Haskell appear in various places. Because Haskell is not dependently typed, they often reduce to the non-dependent version of $\Sigma$-types, which are just Cartesian products. So whenever you see an ordered pair, or a record, that is a simple case of a $\Sigma$-type.

At the level of a modules there can be dependencies and so we get actual $\Sigma$-types. For instance, a module which defines a type $T$ and then a value $f$ of type $T \to T$ has the kind $\Sigma_{T : \mathrm{Type}} (T \to T)$. (The module should hide the definition of $T$ in order for this to actually be the case.) Observe that this is a "large" dependent sum because it ranges over "all Haskell types $T$" so I refer to it as a "kind". In fact, the theory of modules is based on the observation that hiding bits of a program behind a layer of abstraction is precisely the same as forming a dependent sum.

Haskell has existential types. These are like depenent sums of the kind I mentioned above. Namely, an existential type

data Calf = forall t . Bull t =&gt; Cow(t)


is just a confusing way of writing $$\mathtt{Calf} = \textstyle \sum_{t : \mathtt{Bull}} Cow(t).$$ Strangely, the "forall" keywords indicates the fact that there exists a type $t$ of class $\mathtt{Bull}$ such that $F(t)$. Perhaps some Haskellites can explain the logic behind the notation to me.