依存直積
dependent product
https://ncatlab.org/nlab/show/dependent+product