依存直積型の双対

依存ペア型とも言う

↓ほんまか？

\Sigma_{(x:A)}B(x)と表記する

(a,b):\Sigma_{(x:A)}B(x)の意味

a は A 型であり、 b は B(a) である

b の型が、 a の型に応じて変化する