[bgavran]

A coproduct in the category Set is a disjoint union of sets, i.e. A + B + C where A, B, C are sets.

We can think of this coproduct as involving two choices:

1) a choice of which component of the coproduct we're interested in (first, second, or third)

2) a choice of an element of that component

That is, `A + B + C` is isomorphic to `(i : Fin 3 * D i)` where `Fin 3` is a set with three elements, and `D : Fin 3 - > Type` and `D(0)=A`, `D(1)=B`, `D(2)=C`.

Then, the idea is: why index by a finite set? If you replace `Fin 3` by some arbitrary set, you start to be able to model a very general notion of a dependent type.