自己双対コンパクト閉2-圏としての関係圏

本文で話題にしているスピヴァック理論だけど、関係データモデルやERモデルをちゃんと吸収するには、アンビエント圏を関係圏にする必要があるようだ。

で、関係圏なのだが、コンパクト閉圏としては自己双対で、対象の双対は自分自身となる。しかし、射の双対は自分とは限らないので意味を持つ。f:A→B の双対は f^* じゃなくて f^t と書くことにする。関係の転置のほうが一般的だと思うので。

それと、関係圏では、ホムセットに包含順序が入る。順序構造を圏とみなして2-圏（圏で豊穣化された圏）とみなす。これにより、lax自然変換とoplax自然変換を考えることが出来る。lax/oplax変換は、データの時間的な変更を制御するのにどうしても必要。lax/oplax関手が出てくるかどうかはわからない。

転置と順序を使った基本関係は、f:A→B に対して（恒等射とidは同一視して）：

1. f;f^t⊆A
2. A⊆ f;f^t
3. f^t;f⊆B
4. B⊆f^t;f

この4つ。これらを使えば、関係の多重度、重複度、出現性、基数とか呼ばれている性質は記述できる。