集合論的半環宇宙、モデル代数、エルブランモデル

集合圏の部分圏で、isoの族Eが指定されていて、Eに関して亜群になっているようなものUを考える。そして：

1. 空集合と単元集合（少なくとも1つ）を含む
2. A, B∈|U| ならば、A×B∈|U|
3. A, B∈|U| ならば、A+B∈|U|
4. 半環圏としての構造同型がEに入っている。

このような部分圏を集合論的な半環宇宙と呼ぶ。

同値関係〜を持つ集合Aで、次の部分演算を持つものを考える。

1. P:A×A⊃→A
2. S:A×A⊃→A

半環宇宙UからAへの写像fがあって、任意の対象A,Bに対して

1. AとBがEにより同型なら、f(A)〜f(B)
2. f(A)〜a, f(B)〜b となるa, bがあって P(a, b) が定義され、A×Bを表現する。
3. f(A)〜a, f(B)〜b となるa, bがあって S(a, b) が定義され、A+Bを表現する。

その他適当な条件を満たすとき、AはUのモデル代数と呼ぶことにする。特に、Aが適当な項のエルブラン宇宙になっているとき、エルブランモデル代数、あるいは単にエルブランモデル。

型理論の意味論は、集合論的半環宇宙を外的なモデル（概念的なモデル）と考えるのだが、実際の作業はエルブランモデル（＝内的モデル＝実装モデル）を構成することだろう。