RPCの関手モデル的定式化

記法を今までと変える。

1. スキーマは斜体ではなくて普通書体とする。
2. スキーマの対象は小文字 a, b, cなど。
3. スキーマの射は小文字 u, v, wなど。
4. スキーマ射はf, g など。
5. モデルインスタンスはF, Gなど。
6. ドクトリンは斜体 D など。

S, Tがスキーマ、FがT上のインスタンス、HがS上のインスタンスのとき、RPC機構とは、Fの射（F(u):F(a)→F(b) in Partial）をHの射にマップする方法。具体的には、

1. 関手（接続） f:S→T
2. 自然変換 γ::H⇒f^*F 、f^*F は、fによるFの引き戻し。
3. Hのすべての成分は可逆である。

γの成分は、γ_a:H(a)→F(f(a)) となる。これが可逆だから、(γ_a)^-1:F(f(a))→H(a) がPartialで存在する。γの成分ごとに逆にした自然変換をリターンまたはレスポンスと呼ぶ。

Fの射 F(w):F(c)→F(d) がSから起動されることはは、c=f(a), d=f(b), w=f(u) に対する γ_a;F(f(u)) : H(a)→F(f(b)) で記述される、γ_a;F(f(u)) をuに対するリモート実装（の起動）と呼ぶ。リモート実装にリターン（レスポンス）を加えると、リモート呼び出しが完了する。

γがアンビエント圏Partialにおいて可逆なのがミソで、γが引数転送、γ^-1が戻り値転送（逆の転送）となっている。

リモート呼び出しとローカル呼び出しを一緒に考えるには、スキーマSとTの直和（または余極限、融合和）を考えて、そこで議論する。ローカルとリモート（とその中間とか）を混ぜるには、圏の貼り合わせとそれにともなう関手（前層）の貼り合わせを使うことになるだろう。