Is it possible to express sigma-type in Martin-Löf type theory with other constructs In Martin-Löf type theory we have sigma types (dependent products). Is it possible to express them with other constructs? How expressive is dependently typed lambda calculus without them, i.e. what we can't describe without them?
 A: We can completely express $\Sigma$ types in terms of $\Pi$ types in a way that's very reminiscent of Church encoding.  For any given universe $\mathscr{U}$ and any higher universe $\mathscr{U'}$, we may define $\Sigma$ as follows:
$$
\Sigma : \Pi_{A : \mathscr{U}} (A \to \mathscr{U}) \to \mathscr{U'}\\
\Sigma = \lambda A : \mathscr{U} .
         \lambda B : A \to \mathscr{U} .
         \Pi_{C : \mathscr{U}}
         (\Pi_{x : A} B(x) \to C) \to
         C
$$
(This is assuming implicit universe cumulativity, of course, but using explicit universe polymorphism instead doesn't change much anyway.)
The constructor $,$ and the projections $\mathrm{proj}_1$ and $\mathrm{proj}_2$ are similarly defined as follows:
$$
, : \Pi_{A : \mathscr{U}} \Pi_{B : A \to \mathscr{U}} \Pi_{x : A} B(x) \to \Sigma_{x' : A} B(x')\\
, = \lambda A : \mathscr{U} .
    \lambda B : A \to \mathscr{U} .
    \lambda x : A .
    \lambda y : B(x) .
    \lambda C : \mathscr{U} .
    \lambda f : \Pi_{x' : A} B(x') \to C .
    f(x)(y)\\
\mathrm{proj}_1 : \Pi_{A : \mathscr{U}} \Pi_{B : A \to \mathscr{U}} (\Sigma_{x : A} B(x)) \to A\\
\mathrm{proj}_1 = \lambda A : \mathscr{U} .
              \lambda B : A \to \mathscr{U} .
              \lambda v : \Sigma_{x : A} B(x) .
              v(A)(\lambda x : A . \lambda y : B(x) . x)\\
\mathrm{proj}_2 : \Pi_{A : \mathscr{U}} \Pi_{B : A \to \mathscr{U}} \Pi_{v : \Sigma_{x : A} B(x)} B(\mathrm{proj}_1(v))\\
\mathrm{proj}_2 = \lambda A : \mathscr{U} .
              \lambda B : A \to \mathscr{U} .
              \lambda v : \Sigma_{x : A} B(x) .
              v(B)(\lambda x : A . \lambda y : B(x) . y)
$$
The proofs that the expected introduction, elimination, and computation rules and uniqueness principle hold are left to the reader.  :)
