タビュレーション付きダガー表示

ダガー圏の表示として次のものを考える。

• 箙
• 箙のパス等式系

パス等式系は、辺の連接とダガー演算を使った形式的な項のあいだの形式的な等式の集まり。箙から生成した自由ダガー圏を、パス等式系で割り算してダガー圏ができる。

ダガー圏の表示をダガー表示と呼ぶ。Dがダガー表示のとき、生成されたダガー圏をD^◇で表す。ダガー表示D, Eのあいだの射は、D^◇→E^◇ というダガー関手のこと。

Eがダガー表示のとき、E上のタビュレーションとは、集合Tで添字付けられた部分箙の族。正確に言うと：

• Tは集合。
• Eの箙をQ(E)とする。Q(E)の部分箙の全体を Subquiv(Q(E)) とする。
• τ:T→Subquiv(Q(E)) がタビュレーション（tabulation）。

τがタビュレーションであるとき、τ(t)の合併がQ(E)のとき、τはカバリング（被覆）という。被覆になっているタビュレーションだけを考える。

t∈T に対するτ(t)を、tのテーブルスキーマと呼ぶ。τ(t)が結合可能は射のペアを含まないときtは従属性を持たない、という。τ(t)内に結合可能なペアを持つとき、tは従属性を持つ。

箙Q(E)の辺fに対して、f∈τ(t) となるようなtが2つ以上あるとき、τは非直交と呼ぶ。非直交でないタビュレーションを直交タビュレーションと呼ぶ。

ダガー表示E上のタビュレーションτが完全（perfect）タビュレーションだとは：

1. すべてのtが従属性を持たない。つまり、τ(t)内に結合（連接）可能な辺が含まれない。
2. 直交タビュレーションである。

関手 D^◇→E^◇ があると、タビュレーションのあいだのデータ移動も定義できるか？ タビュレーションも関手として定式化できないか？