任意の圏を等式により2-圏とみなす - 檜山正幸のキマイラ飼育記 (はてなBlog)

話したいことはタイトルのとおりの小ネタなんですが、簡単に動機を説明しておきます。

ゴグエン／バーストル〈Joseph Goguen and Rod Burstall〉のインスティチューション〈institution〉は、論理やプログラムの構文論と意味論〈モデル論〉の抽象的枠組みを提供します。抽象度が高いゆえに、一般的で汎用性が高いのですが、ちょっと掴みどころがない感じもします。そこで、抽象的インスティチューションの一部を具体化します。

使う論理を固定する：
抽象的インスティチューションは論理非依存〈logic nutral | logic agnostic〉がウリなんですが、使う論理を等式的論理と一階述語論理に固定します。等式的論理／一階述語論理以外の論理を使いたいケースは少ないからです。
モデルの圏の作り方を固定する：
抽象的インスティチューションのモデルの圏は、公理的に存在が要請されているだけで、どう作るかは指定されてません。が、特殊化されたインスティチューションでは、指標Σのモデルの圏 Model[Σ] は、Model[Σ] := [FreeCat(Σ), Set]_CAT と具体的に与えます。指標Σは有向グラフとみなし、FreeCat(Σ) はΣから作られる自由圏、[-, -]_CAT は“圏の圏”CATの内部ホムです。

等式的論理は、一階述語論理に埋め込めますが、ここでは、等式的論理と一階述語論理を別物として扱います。等式的論理がプライマリであり、一階述語論理は等式的論理のなかで定義されます。一階述語論理なしで等式的論理だけを使うことはできますが、等式的論理なしでは一階述語論理が機能しません。「まずは等式ありき」と考えます。

プライマリな存在である等式的論理を、圏論とスムーズに連携させる手段を考えましょう。連携というよりむしろ、圏論に等式的論理をビルトインする、という感じ。等式は、圏の2-射だとみなします。理屈は簡単なので、記法を決めるだけです。

なお、今回と類似の話が次の記事にあります。

インスティチューションと忘却関手

[追記]続きは「等式的関手インスティチューション（概要）」。[/追記]

内容：

通常圏における2-射とその演算
等式的推論の圏論化

通常圏における2-射とその演算

n-射まで持つn-圏Xの各次元の射の集合（“類＝大きな集合”かも知れない）を次のように書きます。

|X|₀ = |X| = Obj(X) （0-射とは対象のこと）
|X|₁ = Mor(X) （1-射とは射のこと）
|X|₂ = 2-Mor(X) （2-射の集合）
|X|₃ = 3-Mor(X) （3-射の集合）
|X|_k = k-Mor(X) （k-射の集合）

一般的なn-圏の知識は不要で、使うのは2-圏だけです。2-圏では、次の演算があります。

射〈1-射〉の結合
射〈1-射〉と2-射のヒゲ結合〈whiskering〉
2-射の縦結合
2-射の横結合

これらの演算にどのような演算記号を割り当てるかは、目的と趣味により変わります。典型的な2-圏である“圏の圏”では、僕〈檜山〉は次の演算記号を使っています。

演算	図式順記法	反図式順記法
射〈1-射〉の結合	F＊G	G・F
射〈1-射〉と2-射のヒゲ結合	F＊β, α＊G	β・F, G・α
2-射の縦結合	α;β	β $\circ$ α
2-射の横結合	α＊γ	γ・α

射の結合、ヒゲ結合、横結合はすべて同じ記号を使っています。こうするのが一番使いやすいと思います。

さて、Cを通常圏〈ordinary category | 1-圏〉として、Cの2-射を、射〈1-射〉のあいだの等式だとします。

|C|₂ = 2-Mor(C) := {(f, g)∈Mor(C)×Mor(C) | f = g}

この場合の演算記号は、次のように約束しましょう。

演算	図式順記法	反図式順記法
射〈1-射〉の結合	f;g	g $\circ$ f
射〈1-射〉と2-射のヒゲ結合	f;β, α;g	β $\circ$ f, g $\circ$ α
2-射の縦結合	α＆β	なし
2-射の横結合	α;γ	γ $\circ$ α

やはり、射の結合、ヒゲ結合、横結合はすべて同じ記号を使っています。が、“圏の圏”の場合とは違った記号を使います。2-射の縦結合の反図式順演算記号を（使いたい人は）追加してもかまいません。何なら同じ記号'＆'でもさほどの不都合はないでしょう。

上で定義した2-射 (f, g) は、等式 f = g と同じです。2-射であることを強調して、α::f⇒g:A→B in C のようにも書きます。射のあいだの等式は、可換図式でも表現可能です。例えば、f;g = h;k という等式は、次の図式が可換であることと同じです。
$\require{AMScd}\newcommand{\cat}[1]{{\mathcal {#1}}}% \newcommand{\incat}{\:\: \mbox{in}\:}% % \begin{CD} A @>{f}>> B \\ @V{h}VV @VV{g}V \\ D @>{k}>> C \\ \end{CD} \:\:\: \incat \cat{C}$

可換多角形（二角形を含む）を2-射だと思えばいいわけです。あるいは、可換図式をペースティング図だと解釈します。上の図（可換図式＝特別なペースティング図）が表す2-射は、f;g ⇒ h;k : A→C in C です。

等式的推論の圏論化

引き続き、Cは通常圏で、等式をCの2-射と考えます。α::f⇒g:A→B in C と書いたら、f, g∈C(A, B) で f = g なことです。二重矢印記号'⇒'をこの意味で使うので、含意は「ならば」とひらがなで書きます。論理的同値も '⇔'ではなく'iff'（"if and only if"の略記）にします。さっそく使ってみると：

α::f⇒g:A→B in C iff f, g∈C(A, B) かつ f = g

等式を2-射と解釈すると、等式的推論は2-射の計算のなかに吸収されます。

反射律「f = f」は、恒等2-射 ID_f::f⇒f:A→B に相当する。
対称律「f = g ならば g = f」は、α::f⇒g:A→B が可逆であり、縦方向の逆 α^-1::g⇒f:A→B が存在することに相当する。
推移律「f = g かつ g = h ならば f = h」は、α::f⇒g:A→B, β::g⇒h:A→B の縦結合 α＆β ::f⇒h:A→B が存在することに相当する。

F:C→D が（通常の）関手だとして、Fは2-射のレベルまで自然に拡張できます。次のように記号の約束をしましょう。

F_obj:|C|₀→|D|₀
F_mor:|C|₁→|D|₁
F_eq:|C|₂→|D|₂

F_objとF_morはいつもどおり（特に変わったことなし）です。F_eq は、(f, g)∈|C|₂ に対して、

F_eq((f, g)) := (F(f), F(g)) ∈|D|₂

として定義されます。f = g ならば F(f) = F(g) なので、この定義は well-defined です。つまり、通常の関手〈ordinary functor〉Fから、2-射部分 F_eq:|C|₂→|D|₂ は自動的に（あるいはタダで）定義できます。

関手Fの2-射部分（あるいは等式部分）F_eq:|C|₂→|D|₂ は、2-射の演算を保存します。

F_eq(α＆β) = F_eq(α)＆F_eq(β)
F_eq(α;γ) = F_eq(α);F_eq(γ)

これは当たり前のことですが、等式的推論の基本的なことなので説明します。α::f⇒g:A→B, β::g⇒h:A→B, γ::j⇒k:B→C としましょう。2-射＝等式は、両端（左辺と右辺）が決まれば決まるので、α = (f⇒g:A→B), β = (g⇒h:A→B), γ = (j⇒k:B→C) とも書きます。

α = (f⇒g:A→B), β = (g⇒h:A→B) から縦結合 α＆β を作る過程は、次のような等式的推論です。

  f⇒g:A→B  g⇒h:A→B
 ---------------------- 等号の推移性
      f⇒h:A→B

これはC側での推論ですが、関手Fを経由してD側の推論になります。

  F(f)⇒F(g):F(A)→F(B)  F(g)⇒F(h):F(A)→F(B)
 ----------------------------------------------- 等号の推移性
      F(f)⇒F(h):F(A)→F(B)

これが F_eq(α＆β) = F_eq(α)＆F_eq(β) の意味です。'＆'は、等号〈等値関係〉の推移性を使って新しい等式を作る演算なのです。

F_eq(α;γ) = F_eq(α);F_eq(γ) も同様に、C側の等式的推論と、D側の等式的推論を示します。

  f⇒g:A→B  j⇒k:B→C
 ---------------------- 辺々を結合
     f;j⇒g;j:A→C

  F(f)⇒F(g):F(A)→F(B)  F(j)⇒F(k):F(B)→F(C)
 --------------------------------------------- 辺々を結合
     F(f);F(j)⇒F(g);F(j):F(A)→F(C)

このようにすると、等式の扱いは2-射（一般的には、n-圏の(n+1)-射）として圏にビルトインされます。圏は等式的論理を最初から（ビルトイン〈組み込み〉で）持つことになります。

冒頭で述べた、インスティチューションで使う等式的論理とは、圏にビルトインされた等式的論理のことです。等式的論理が一階述語論理に先行するとは、圏の内部で一階述語論理を作るので、圏が最初から持つ機能である等式的論理は当然使うよ、ってことです。

[追記]続きは「等式的関手インスティチューション（概要）」。[/追記]