[atennapel]

Your `Sum` is actually a `Pair` as well :). Should be: ``` Sum A B = (C : *) -> (A -> C) -> (B -> C) -> C ```

Note that in the calculus of constructions you can do these Church encodings of datatypes but you cannot derive an induction principle for these (only non-dependent folds). For example you cannot write a `snd` for the `Sigma` above.

As you allude to, you need a more expressive type system to derive induction principles (for example "Self types") for lambda encodings.