二重圏と一様性、2-セルによる定式化
関連するエントリーは次：
- (仮称)一様性二重圏
- セリンガーのND補題
- 一様性を持つ部分トレース付き圏の周辺
- 一様性を持つ部分トレース付き圏（partially traced category with uniformity）
- 一様性原理
次の言葉を使う。
- 一様射（uniform morphism）セリンガーに従う
- 一様クラス（uniform class） 一様射の全体
- 垂直射 本来二重圏の概念だが、境界を境界に移す射、入出力変換
- 垂直クラス 垂直射の全体
圏Cはトレース付きモノイド圏で、一様クラスUと垂直クラスHが指定されているとする。一様クラスは長谷川／セリンガー／ステファネスクなどが考察しているアレである。垂直クラスの最も簡単な例は、idだけからなるクラス（射の集まり）である。
Circ構成で、f:A+X→B+X を、f/X:A→B と書くことにする。f+g もf/g のような分数記法を使う。後の計算例では、A+Bは縦（Aが上）に並べるだけでf+gだけ分数にしている（統一性がないがいいとする）。f:A+X→B+Y が分数では書けない（f=f1+f2とならない）、または書く必要がないことを強調して A/X |f| B/Y のように書く（後の計算例を参照）。計算記法が未成熟だが、今のところ、こういう暫定記法を採用している。
f/X:A→Bとf/Y:A'→B'がCのCirc圏の射だとする。もちろん、Cで見れば f:A+X→B+X、g:A'+Y→B'+Y ということ。α=α/uがf/Xからg/Yへの2-セルであるとは次のこと：
- a:A→A', b:B→B' は垂直射である。
- Cにおいて、f;(b+u) = (a+u);g が成立する。
αは (a, b, u)の3つ組となるが、特にuを強調してα/uとも書く。上の計算は、2-セルα、βの結合がまた2-セルになること。モノイド圏の交替律しか使ってないが、次の事実は仮定している。
- 垂直射の結合は垂直射
- 一様射の結合は一様射
つまり、U⊆C, H⊆C が部分圏となっている。この状況で2-セルは双模倣であり、一様性原理は次のように述べられる。
- Tr(f/X);b = a;Tr(g/Y)
しかし、これでも一般性が不足。元の圏Cが2-圏だとして
- Cにおいて、φ::f;(b+u)⇒(a+u);g なら、ψ::Tr(f/X);b⇒a;Tr(g/Y) がある。
という形にしたい。上の状況で、 入力変換a、出力変換b、状態空間の模倣写像（simulation map）u、模倣関係φがあるとき、振る舞いのあいだにも模倣関係ψがあると解釈できる。φやψを関係と呼ぶと混乱しそうだから、模倣表明（simulation assertion）がいいかな。
