(仮称)一様性二重圏

トレース、隠蔽（hiding）、模倣、関数性、内部意味論などの定式化のために二重圏を使うことを考えている。とりあえず、二重圏の用語法を固定しておく。D = (D₀, D₁, ι:D₀→D₁, δ, γ:D₁→D₀)が二重圏として：

Obj(D0)	対象
Mor(D0)	垂直射
Obj(D1)	水平射
Mor(D1)	セル
comp(D0)	垂直射の垂直結合
comp(D1)	セルの垂直結合
comp(D)	水平射／セルの水平結合

Dの垂直射の圏（D₀）をDの垂直圏と呼び V_Dと書く。単にVとも書く（V=D₀である）。Dの水平射の圏（Obj(D₀)とObj(D₁)からなる圏）をH_Dと書く。単にHとも書く。

次の状況を考える。

1. V, Hにはモノイド構造が入っている。|V|=|H|でモノイド積は共通。
2. 閉包トレースtrは、H(A, B)→H(A, B)という写像である。
3. 隠蔽hd_Xは、H(A×X, B×X)→H(A, B)である。
4. tr;tr = tr, hd;tr = tr;hd;trなどを満たす。
5. tr(f) = f であるfを関数射と呼ぶ。
6. trもhdもトレースのように振る舞う。特に、関数射に対するhd;trは通常のトレースTrを再現する。
7. i:A→A', j:B→B'が垂直射、α::(f:A→B)⇒(g:A'→B') がi, jを境界とするセルのとき、tr(f);j = i;tr(g) : A→B' in H が成立する。

最後の条件は一様性原理で、セルαが模倣であることを定式化している。i, jは入出力の変換である。α::f→g があるとき、fとgはあまり区別できないことを意味する。

D全体を公理化するのは難しい。一様トレース圏（Uniformly traced category）Cから作ったDで調べよう。Cの一様性（uniformity, uniform class, the class of uniform morphisms）をUとする。

1. Dの対象はCの対象。
2. Dの垂直射はCの射。
3. Dの水平射f:A→Bは、Cの射f:A×X→B×X。Xをfの状態対象または隠蔽対象（hidden object）と呼び、f:A→B /X のように書く。
4. Dのセルα::(f:A→B /X)⇒(g:C→D /Y)は、(i:A→C, j:B→D in C; u:X→Y in U)のこと。ただし、(i×u);g = f;(j×u) : A×X→D×Y が成立している。

Dのセルの定義（Cの一様性原理）から、Dで一様性「α::f→g ⇒ tr(f);j = i;tr(g)」が成立する。

課題： 知られているCから二重圏Dを作れ。Cは、エルゴット・オートマトンの圏、有限ラベル付き遷移系の圏、コンポネントの圏など。