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.
- Dependent sum
- Cartesian product - Disjoint union EDIT: Ah, started writing before you edited; yeah, (with an expressive enough type system) lambda's all you need