"Even more, this coproduct can be thought of as an instance of a dependent pair indexed by a finite set" - I know what the individual terms mean, but I don't get what this is saying.
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.
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.