Here is a short note for the bulletin board: I agree with Mike Barr that "dependent function" and "dependent product" express exactly what is going on and should be the terminology used. It is a THEOREM that a dependent product is a kind of sum, generalizing the well known fact that in sets A\x B is a sum of A copies of B. A similar remark applies to dependent functions. However, the introduction of the names "dependent product" for dependent function and "dependent sum" for "dependent product" has expelled us permanently from Paradise. The confusion would be as bad as it has been for the notation for set inclusion, which was irretrievably messed up when in the sixties people started using the sideways horseshoe to mean "included in but not equal to" instead of merely "included in", which had been the standard meaning for fifty years. What about "indexed product" and "indexed sum"?