ここ2,3日考えていたことがあります。その動機とか背景とかを説明すると「けっこう面白い」かと思うのですが、長くなるので結論（になるはずのこと）だけをザッと述べます。一言だけいっておくと、大量のモナド類似物（monad-like entities*1）を一挙に扱う方法が欲しくてなにやらゴニョゴニョしています。
内容：
概略
インデックス付き圏とは、結局は、圏の圏Catに値を持つ関手に過ぎません。細かいことを気にしなければ、圏Yをインデックスの圏とするインデックス付き圏の全体 IndCat[Y] のような圏を定義できます。そして、IndCat[Y] への関手 X→IndCat[Y] のような概念も定義できます。これは、繰り返された（あるいは入れ子の）インデックス付き圏と考えることができます。
一方で、圏の直積をインデックスとするインデックス付き圏 X×Y→Cat を考えることもできます。こちらは二重インデックス付き圏と呼んでいいでしょう。より一般には多重インデックス付き圏ですね。
繰り返されたインデックス付き圏 X→IndCat[Y] と二重インデックス付き圏 X×Y→Cat の間に対応を付けることができます。これは、圏の圏Catがデカルト閉であることから、関手のカリー化／反カリー化を行えるからです。
さて、インデックス付き圏からインデキシングを忘れた圏を作る手順がグロタンディーク構成（Grothendieck construction）です。通常、グロタンディーク構成というと、インデックス付き圏 → ファイバー付き圏（fibred/fibered category）という対応を意味することが多いので、ここでは、ファイバー付きではない単なる圏を作ることをグロタンディーク平坦化と呼びましょう。
繰り返されたインデックス付き圏に2回グロタンディーク平坦化を行うことは、二重インデックス付き圏に対して一気にグロタンディーク平坦化するのと同じ、とたぶん言えます。実は、ちゃんと細部まで確認してなくて、状況証拠と類推から言っているので、間違っている可能性もあります。ですが、少なくともある条件のもとでは成立してる実例があります。
記法を工夫すると、この主張は、積分に関するフビニ（Fubini）の定理と似た形になります。フビニの定理は、ある条件のもとでは多重積分と繰り返し積分（逐次積分）の値が等しくなると述べています。同様に、ある条件のもとでは、多重グロタンディーク平坦化と繰り返しグロタンディーク平坦化で得られる圏が圏同値だろうと思えます。この圏同値があるとすれば、それをフビニ／グロタンディーク同値と呼んでもいいでしょう。
関手圏の記法
C, Dが圏だとして、CからDへの関手を対象として、自然変換を射とする圏（関手圏）を [C, D] で表します。反変関手から作られる圏のほうは上付き星印を付けて [C, D]* とします。記号のバランスを取るために、共変関手の圏 [C, D] に下付きの星印を付けることもあります。まとめると次のようです。
- [C, D]* = [C, D]
- [C, D]* = [Cop, D] = [C, Dop]
圏のサイズの問題を度外視すれば、[C, D] は圏の圏Catのホムセット Cat(C, D) でもあり、Catの指数 DC でもあります。
圏の圏Catがデカルト閉であることから、次の2つの関手圏は圏同値になります。
- [C, [D, E]]
- [C×D, E]
この記法を使うと、インデックス付き圏は IndCat[Y] = [Y, Cat]* と書けます。
関手のラムダ記法
Fが関手 C→D のとき、それを対象部分と射部分に分けてラムダ記法で書けば次のようになるでしょう。
- Fobj = λA∈Obj(C).F(A)
- Fmor = λf∈Mor(C).F(f)
対象にも射にも、どちらにでもなれる変数xを使って書けば：
- F = λx∈C.F(x)
ここでラムダ記法を使ってもあまり有難味がないように思えますが、多変数の関手のときは意味があります。例えば、F:C×D→E のとき、次の2つの式は違う意味を持ちます。
- λx∈C.F(x, y)
- λy∈D.F(x, y)
多変数関手の変数の一部を束縛するときにラムダ記法は便利なのです。
変数が走る範囲が前もって明らかなら、λx.F(x)、λx.F(x, y) のような書き方も許しましょう。さらに、λの代わりにδを使ってピリオドを省略した形 δx F(x)、δx F(x, y) でもいいとします。
なんでいきなり「δ」が出てきたんだ？ と訝しく思うでしょうが、これは、被積分項となる微分形式 f(x) dx を意識した形です。被積分項を dx f(x) と書くこともたまにはあります。dx f(x) のなかで変数xは束縛されているので、dy f(y) のように置き換えても意味は変わりません。同様に、δx F(x) = δy F(y) です。
グロタンディーク平坦化の記法
Fが圏X上のインデックス付き圏であるとは、F:X→Cat （反変）のことなので、F∈[X, Cat]* と書けます。習慣により、F(x) ではなくて F[x] と書くこともあるので、F(x) と F[x] は同じ意味だとします。ここで変数xは、圏X上の対象にも射にもなれる変数です。
インデックス付き圏 F:X→Cat のグロタンディーク平坦化を ΣX(δx F[x]) と書きましょう。δx F[x] は、先ほど述べたように、Fそのものを微分形式風に表記したものです。Σは総和記号です。積分記号のほうがふさわしいと思いますが、積分記号は既にエンド／余エンドの意味で使われているので総和記号にしました。
インデックス付き圏は、反変関手として定義されていますが、共変で使うときもありますし、XとXopを入れ替えれば同じことなので、以下では記号が簡単になるように共変関手として扱うことにします。
ΣX は、[X, Cat]→Cat という対応になります。ΣX(F) = ΣX(δx F[x]) です。微分形式風の書き方が意味を持つのは、Fが X×Y→Cat や X → [Y, Cat] のときで、ΣX×Y(δ[x, y] F[x, y]) とか ΣXδx(ΣY(δy F[x, y])) などの書き方ができます。
フビニ／グロタンディーク同値
ここまで記法の準備ができれば、フビニ／グロタンディーク同値の記述は簡単です。しかし、冒頭でも注意したように、記述ができてもそれが正しい保証はありません。実際にフビニ／グロタンディーク同値を使うときは、当該のインデックス付き圏にはナニヤラ付加的構造や条件が付いているのが普通なので、それらも含めて議論するとややこしいと思います。
F:X→[Y, Cat] がインデックス付き圏に値を持つような関手（これも一種のインデックス付き圏とみなします）、Fの反カリー化である関手をF~とします； F~:X×Y→Cat 。逆に、Fが X×Y→Cat として与えられているときは、Fのカリー化 F^ が F^:X→[Y, Cat] となります。いずれのケースでも、与えられたFとそのカリー化／反カリー化を同じ記号で表してしまう、とします。この約束のもとで、次の2つの圏のあいだの圏同値がフビニ／グロタンディーク同値です。
- ΣXδx(ΣY(δy F[x][y]))
- ΣX×Y(δ[x, y] F[x, y])
実例
大域環境として使える型の全体からなる圏をXとして、X∈X （ローマンが対象、イタリックが圏）を固定した上で、Xを参照して例外Yを出すかもしれない計算の圏を F[X][Y] とします。Xを固定したまま対象Yを圏Y内で動かし、射に関しても適切な定義をすると、F[X] は圏Y上のインデックス付き圏になります。つまり、繰り返されたインデックス付き圏です。対応する二重インデックス付き圏は、大域環境と例外を同時に考えた圏の集まりです。
以上のセッティングで、どのような手順を経ても同値なグロタンディーク平坦化が得られることが、フビニ／グロタンディーク同値の例です。
