自然演繹のための構成法
- Cは一般的なモノイド圏、X = (X, δ, ε)がC内の余モノイド(余モノイド構造、余モノイド対象)のとき、Xのスタンピング関手(域側に掛け算する)から余モナドが定義できる。
- 上記の余モナドの余クライスリ圏を作れる。これは一般的な構成。
- 余モナドがテンソル強度(余テンソル強度)を持つとき、余クライスリ圏がプレモノイド圏になる。特に可換余モナドなら余クライスリ圏はモノイド圏となる。
- Cがデカルト圏なら、すべての対象が余モノイドになる。したがって、余クライスリ圏が作れる。
- それだけではなくて、スタンピング余モナドが可換余モナドとなるので、余クライスリ圏はモノイド圏となる。
- さらに、そのモノイド積はデカルト・モノイド積なので、出来た余クライスリ圏はデカルト圏となる。
- 与えられたデカルト圏から余クライスリ・デカルト圏を作る構成法は、CartCat→CartCatという関手になる。この構成に特に名前がないのでB-構成と呼ぶことにする。
- B-構成は、{環境 | 文脈 | 背景}付き計算の定式化になっている。
- B-構成で使うXを動かすと、C上のCartCat値のインデックス付き圏が出来る。これはインデックス付きB-構成〈indexed B-construction〉。
- そのグロタンディーク平坦化も出来る。