圏論の計算のために、テキストエディタとキーボードだけでも容易に入力可 能な記法を提案し、計算を実行してみる。この記法は、図式順（diagrammatic order）に左から右に向かって書き記す方式である。
圏論の計算のために、テキストエディタとキーボードだけでも容易に入力可 能な記法を案出しようと何度か試みて、何度か（試みと同じ回数）挫折した。 それで得た教訓は、あまり高望みせず（所詮、テキスト表現では限度があるから）、 できることだけをチマチマとやっていくほうがよさそうだ、ということ。それ で、自然変換の計算にしぼって、アスキー文字＋ギリシャ文字(*注1)で書け る記法を提案し、計算を実行してみる。
英字に対する太字、下線など修飾が使えれば、それをギリシャ文字の代わり に使える。
テキストによる式は、diagrammatic order、つまり左から右に読めること に拘った。この特徴を強調して、ここで述べる記法を‘図式順テキスト記法 （Diagrammatic-Order Text Notation; DOTN）’と呼ぶことにする。左から右 の記法を使う人は多くはない。 Juergen Koslowskiが使って いるのを見たことがあるが、どうも違和感がある。一方、 Roland Backhouseは右から左を徹 底している（図式も右から左を使う）が、これはこれで読みにくい。DOTNも当 然に違和感をまぬがれないだろうが、表記と計算の機能性はなかなか優れてい る。とりあえず、自然変換の縦結合と横結合の交替律（interchange law）を DOTNで示すことをこの記事の目標とする。
記号を次のように使い分ける。まったく厳密密性に欠ける規則だが、人間の “常識”で理解可能ならよいとする（コンピュータ処理は度外視）。
特に断りがなくても、a∈Cは、aがCの対象であることを示す。上の規約から、 aのタイプは圏の対象だから紛れることはないだろう。また、f∈Cは、fがCの 射であることを示し、f:a→b in C は、f∈C で f:a→b であることを示す。
fとgの（この順での）結合（composition;合成）はf;gと書く。対象aの恒等 射はa^で示す。f:a→b, g:b→c, h:c→d in C として次が成立する。
f:a→b in C、F:C→D、G:D→E のとき、
記法の約束からただちに次が従う：
a.F -[f.F]→b.F a.α| |b.α | | in D v v a.G -[f.G]→b.G
自然変換α::F⇒G:C→D、β::G⇒H:C→Dに対して、自然変換 (α|β)::F⇒ H:C→Dを次のように定義する。
(α|β)を、αとβの‘縦結合’と呼ぶ。 (α|β)が、F⇒H:C→Dの自然変換になることは、次を示せばよい（下図参照）。
in D a.F -[f.F]→b.F a.α| |b.α | (1) | v v a.G -[f.G]→b.G a.β| |b.β | (2) | v v a.H -[f.H]→b.H
これは次のように計算できる。
αとβの自然性を仮定する。 (1) a.α;f.G = f.F;b.α (2) a.β;f.H = f.G;b.β a.(α|β);f.H //↓ |の定義 = (a.α;a.β);f.H //↓ ;の結合律 = a.α;(a.β;f.H) //↓ 仮定(2) = a.α;(f.G;b.β) //↓ ;の結合律 = a.α;f.G;b.β f.F;b.(α|β) //↓ |の定義 = f.F;(b.α;b.β) //↓ ;の結合律 = (f.F;b.α);b.β //↓ 仮定(1) = (a.α;f.G);b.β //↓ 括弧をはずして書いただけ = a.α;f.G;b.β
関手F:C→Dに対して、自然変換ι::F⇒F:C→Dを次のように定義する。
a.F -[f.F]→b.F a.ι| |b.ι | | in D v v a.F -[f.F]→b.Fこれは次のように計算できる。
a.ι;f.F //↓ ιの定義 = (a.F)^;f.F //↓ idの性質 = f.F f.F;b.ι //↓ ιの定義 = f.F;(b.F)^ //↓ idの性質 = f.F
以上で定義したιはF:C→Dごとに決まるので、これをF^を書く。この記号で改めて定義を書くと：
α::F⇒G:C→D のとき：
次のように計算できる。
f:a→b in C a.(F^|α) //↓ |の定義 = a.F^;a.α //↓ F^の定義 = (a.F)^; a.α //↓ idの性質 = a.α a.(α|G^) //↓ |の定義 = a.α;a.G^ //↓ G^の定義 = a.α;(a.G)^ //↓ idの性質 = a.α
α::F⇒G:C→D、β::G⇒H:C→D、γ::H→K::C→Dに対して、次の結合律も簡 単に示せる。
a.((α|β)|γ) //↓ |の定義 = a.(α|β) ; a.γ //↓ |の定義 = (a.α ; a.β) ; a.γ //↓ ;の結合律 = a.α ; (a.β ; a.γ) //↓ |の定義 = a.α ; (a.(β|γ)) //↓ |の定義 = a.(α|(β|γ))
いままでの結果から、F:C→Dの形の関手を対象として、α::F⇒G:C→Dの形の 自然変換をFからGへの射とする圏が定義できた。対象F（実体は関手）に対す る恒等射（実体は自然変換）はF^、圏の結合（合成）演算は|（自然変換の縦 結合）で与えられる。
F:A→B、β::G⇒H:B→C、K:C→Dだとする。このとき、F;;β :: F;;G⇒F;;H : A→C と β;;K :: G;;K⇒H;;K : B→D を次のように定義する。a∈A、b∈ Bとして：
次の計算で示せる。
a.(F;;β);f.(F;;H) //↓ F;;βとF;;Hの定義 = a.F.β;f.F.H //↓ 括弧を付ける = (a.F).β;(f.F).H //↓ 仮定 -- βが自然変換 = (f.F).G;(b.F).β //↓ F;;GとF;;βの定義 = f.(F;;G);b.(F;;β) x.(β;;K);g.(H;;K) //↓ β;;Kと H;;Kの定義 = (x.β.K);(g.H.K) //↓ Kの関手性 = (x.β;g.H).K //↓ 仮定 -- βが自然変換 = (g.G;y.β).K //↓ Kの関手性 = g.G.K;y.β.K //↓ G;;Kとβ;;Kの定義 = g.(G;;K);y.(β;;K)
次の形の分配律が成立する。F:C→D、β::G⇒G':D→E、β'::G'⇒G :D→E ； α::F⇒F':C→D、α'::F'⇒F :C→D として：
a.(F;;(β|β')) //↓ ;;の定義 = a.F.(β|β') //↓ |の定義 = a.F.β ; a.F.β' //↓ ;;の定義 = a.(F;;F) ; a.(F;;β') //↓ |の定義 = a.((F;;F)|(F;;β'))
a.((α|α');;G) //↓ ;;の定義 = a.(α|α').G //↓ |の定義 = (a.α ; a.α').G //↓ Gの関手性 = a.α.G ; a.α'.G //↓ ;;の定義 = a.(α;;G) ; a.(α';;G) //↓ |の定義 = a.((α;;G)|(α';;G))
α:: F⇒F' :A→B、β:: G⇒G' :B→Cという2つの自然変換を考える。 これらに対して、‘横結合’（スター積）α*βを次のように定義する。
この定義がαとβに対して“対称性”を持つこと： (α;;G)|(F';;β) = (F;;β)|(α;;G') を示したい。そのための補題を得るため、a.α:a.F→a.F' in B に対してβ::G⇒G':B→Cを適用する。
a.F.G -[a.α.G]→a.F'.G a.F.β ｜ ｜a.F'.β ↓ ↓ a.F.G' -[a.α.G']→a.F'.G'これより、a.F.β ; a.α.G' = a.α.G ; a.F'.β。これを使って目的の等式 を示す。
a.((α;;G)|(F';;β)) //↓ |の定義 = a.(α;;G);a.(F';;β) //↓ ;;の定義 = a.α.G ; a.F'.β a.((F;;β)|(α;;G')) //↓ |の定義 = a.(F;;β);a.(α;;G') //↓ ;;の定義 = a.F.β ; a.α.G' //↓ 上の補題 = a.α.G ; a.F'.β
よって、α*βは次のように定義してもよい。
実際には、次の形の定義が有効である。
以下の計算では、上の定義を用いる（別な定義を採用したほうが簡単になる こともあるが）。
ここでも、α:: F⇒F' :A→B、β:: G⇒G' :B→C、γ:: H⇒H' :C→D とする。 関手A^:A→Aに対応する恒等自然変換をA^^::A^⇒A^:A→A とする。^の定義より。
A^^ をA~と略記することもある。つまり：
横結合に関して、次が成立する。
定義：a.(α*β) = a.α.G ; a.F'.β を使う。ブラケットは丸括弧と同じ。 a.((α*β)*γ) //↓ *の定義 = a.(α*β).H ; a.(F';;G').γ //↓ 括弧を付ける = [a.(α*β)].H ; a.(F';;G').γ //↓ *の定義 = [a.α.G ; a.F'.β].H ; a.(F';;G').γ //↓ 括弧をはずす = a.α.G.H ; a.F'.β.H ; a.F'.G'.γ a.(α*(β*γ)) //↓ *の定義 = a.α.(G;;H) ; a.F'.(β*γ) //↓ 括弧の付け替え = a.α.(G;;H) ; [(a.F').(β*γ)] //↓ *の定義 = a.α.(G;;H) ; [(a.F').β.H ; (a.F').G'.γ] //↓ 括弧をはずす = a.α.G.H ; a.F'.β.H ; a.F'.G'.γ
定義：a.(α*β) = a.α.G ; a.F'.β を使う。 a.(A~*α) //↓ *の定義 = a.A~.F ; a.A^.α //↓ A~の定義 = a^.F ; a.A^.α //↓ A^の定義 = (a.F)^ ; a.α //↓ idの性質 = a.α
定義：a.(α*β) = a.α.G ; a.F'.β を使う。 a.(α*B^) //↓ *の定義 = a.α.B ; a.F'.B~ //↓ B~の定義 = a.α.B ; (a.F')^ //↓ Bの定義 = a.α ; (a.F')^ //↓ idの性質 = a.α
定義：a.(α*β) = a.α.G ; a.F'.β を使う。 a.(F^*β) //↓ *の定義 = a.F^.G ; a.F.β //↓ F^の定義 = (a.F)^.G ; a.F.β //↓ Gの関手性 = (a.F.G)^ ; a.F.β //↓ idの性質 = a.F.β //↓ ;;の定義 = a.(F;;β)
定義：a.(α*β) = a.α.G ; a.F'.β を使う。 a.(α*G^) //↓ *の定義 = a.α.G ; a.F'.G^ //↓ G^の定義 = a.α.G ; (a.F')^ //↓ idの性質 = a.α.G //↓ ;;の定義 = a.(α;;G)
定義：a.(α*β) = a.α.G ; a.F'.β を使う。 a.(F;;G)^ //↓ 関手の^の定義 = (a.(F;;G))^ //↓ ;;の定義 = (a.F.G)^ a.(F^*G^) //↓ *の定義 = a.F^.G ; a.F.G^ //↓ F^、G^の定義 = (a.F)^.G ; (a.F)^ //↓ Gの関手性 = (a.F.G)^ ; (a.F)^ //↓ idの性質 = (a.F.G)^
α::F⇒F':A→B、α'::F'⇒F :A→B、β::G⇒G':B→C、 β'::G'⇒G :B→C に対して次が成立する。
先に次の等式を示しておく。
a.α': a.F'→a.F'' in B に β::G⇒G':B→Cを適用すると： a.F'.G -[a.α'.G]→ a.F''.G a.F'.β ｜ ｜a.F''.β ↓ ↓ a.F'.G' -[a.α'.G']→ a.F''.G'
交替律は次のように計算される。
(*) a.α'.G;a.F''.β = a.F'.β;a.α'.G' in C を使う。 a.((α|α')*(β|β')) //↓ *の定義 = a.(α|α').G ; a.F''.(β|β') //↓ |の定義 = (a.α;a.α').G ; (a.F''.β;a.F''.β') //↓ Gの関手性 = (a.α.G;a.α'.G) ; (a.F''.β;a.F''.β') //↓ 括弧の付け替え = a.α.G;(a.α'.G;a.F''.β); a.F''.β' //↓ (*)を使う = a.α.G;a.F'.β;a.α'.G';a.F''.β' a.((α*β)|(α'*β')) //↓ |の定義 = a.(α*β) ; a.(α'*β') //↓ *の定義 = (a.α.G;a.F'.β);(a.α'.G';a.F''.β') //↓ 括弧をはずす = a.α.G;a.F'.β;a.α'.G';a.F''.β'