モノイド二重圏（monoidal double category）というものを使ってみようと思っているんですが、これに関連した計算問題があります。さきほど思いついたもので、Webを探せば答は見つかるような気がしますが、気力・体力がある人にはいい練習かな、と。僕は、気力・体力がないのでやりません。
終対象と引き戻し（ファイバー積）を持つ圏Cに対して、Cat(C) は、Cにおける内部圏の圏とします。Cにおける内部圏とは、Cの対象 A0, A1 と射 d0, d1, i, c の組 (A0, A1, d0, d1, i, c) で、これが圏の構造を持つものです。内部圏の準同型である内部関手も、関手の定義をCのなかで記述すれば得られます。Cat(Set) = Cat と考えることができます。
小さい二重圏と小さい二重圏の圏は、DblCat = Cat(Cat) として得られます。面倒になるのを厭わないなら、直接的具体的に二重圏を定義することもできます。
さて、モノイド二重圏とは、二重圏にモノイド積の構造が入ったものですが、その定義として次の二つが思いつきます。
- Cat(MonCat)
- Mon(DblCat)
MonCatはモノイド圏の圏*1で、Mon(-) は圏に内部モノイドの圏を対応させる構成法です。
ぱっと見、この二つの定義は同値のように感じます。Cat(Mon(Cat)) = Mon(Cat(Cat)) と書いてみると、Cat(-) と Mon(-) が順序交換するとも読めます。Mon(-) は単体圏Δを使って、Mon(C) = [Δ, C] = Cat(Δ, C) と書けるので、Mon(-) はΔで表現できます。もし Cat(-) に表現対象Γがあるなら、[Γ, [Δ, C]] = [Δ, [Γ, C]] = [Δ×Γ, C] とかなると都合がいいですね*2。単なるカリー化になるので。
Cat(MonCat) = Mon(DblCat) が成立してもしなくても、モノイド二重圏を使う側としてはナントカナルのですが、いくつかの定義の「どれを使ってもいいよ」となると、便利だし安心感もあります。誰か確認してみてよ。
