PS

Disjoint union

定義 Dependent type

Union, 和集合

集合族 (A_i)_{i \in I} について

  • \lbrace x \mid {} ^ \exists i \in I, x \in A_i \rbrace

を

  • \bigcup\limits _ {i \in I} A _ i

と書き、集合族 (A _ i) _ i のunionと呼ぶ。つまり、

  • (\exists i \in I, x \in A _ i) \Leftrightarrow x \in \bigcup\limits _ {i \in I} A _ i

Disjoint union

集合族 (A _ i) _ {i \in I} について

  • \bigcup\limits _ {i \in I} \lbrace (i, x) \mid x \in A _ i \rbrace

を

  • \biguplus\limits _ {i \in I} A _ i

と書き、集合族 (A _ i) _ i のdisjoint unionと呼ぶ。

Coproduct

圏論においては、 \biguplus の代わりに \coprod が使われ、coproductと呼ばれる。

Dependent sum

型理論においては、 \biguplus の代わりに \Sigma や \exists が使われ、existential typeと言われる。 特に、型を添字集合とする型族の和集合をdependent sumという。

forSome

Scalaでは、forSomeというのがある。(添字 i は与えられない)
型の集合をとすると、

記法

  • \bigcup A \equiv \bigcup \lbrace A _ i \mid i \in I \rbrace = \bigcup\limits _ {i \in I} A _ i

参考文献