依存和型
dependent sum types
依存直積型
の
双対
依存ペア型
とも言う
#WIP
↓ほんまか？
$ \Sigma_{(x:A)}B(x)
と表記する
$ (a,b):\Sigma_{(x:A)}B(x)
の意味
a
は
A
型であり、
b
は
B(a)
である
b
の型が、
a
の型に応じて変化する
https://ncatlab.org/nlab/show/dependent+sum+type
https://ja.wikipedia.org/wiki/依存型#依存ペア型