Indexed categoriesの紹介記事を昨日書き始めました。すべてのindexed categoriesは（適当に構造を定義すれば）、ひとつのindexed categoryになると僕は信じているのですが、基礎論的にはかなり胡散臭く、あやしい。
僕は多少危ない橋でも神経質になることはないけど、次のような論法はいかがなもんでしょうね？
- 圏Iから“圏の圏”Catへの反変関手C:I→Catがindexed categoryである（定義）。
- C:I→Cat、D:I→Catが2つのindexed categoriesであるとき、C;f=Dとなる関手f:Cat→Catとの3つ組(C, D, f)を射C→Dと考えると、圏IndCat[I]が定義できる。
- よって、I → IndCat[I] という対応は、Iに圏を割り当てている。
- 関手α:I→Jがあるとき、引き戻し（pull backではなくてpre-compose）α* によって、IndCat[J]→IndCat[I]が定義できる（おおむね、α*(D, E, g) = (α*(D), α*(E), g)）。
- よって、I → IndCat[I] と α → α* の組は、Cat→Cat反変関手を定義する。
- これは、Iを特にCatとしたindexed categoryに他ならない。
うーん、いかがわしい。
コーヒーでも飲みながら考えてみよう。
