シーケント計算は論理の計算手法ですが、圏論との関係が深いことがわかっています。であるなら、圏論から出発してシーケント計算を構成してはどうでしょうか。やってみます。
内容：
記号の使い方
以下で、A、B、Cなどは論理式あるいは命題を表します。じゃ、命題って何だ？ と言うと、別になんでもかまいません。今回は圏の対象のことを命題と呼ぶことになります。Γ、Δ などのギリシャ文字大文字は、命題をカンマで区切って並べた列を表します。カンマの意味は圏のモノイド積（後述）です。
シーケントの左右の区切りは「→」を使います。「⇒」や「|-」もよく使われますが、ここでは「→」です。推論の仮定は横棒の上段に、結論は下段に書きます。
論理記号は、「I」（大文字アイ）、「∧」、「⊃」の3つですが、「∧」は明示的に使う必要がないので登場しません。別に明示的に使ってもいいのですが、カンマで代用できるので入れてないだけです。
シーケント計算の特徴である（と誤解されている）構造規則は、今回は使わないでやってみます*1。公理と推論規則だけです。公理は、仮定（上段）がカラッポな推論規則とみなせるので、推論規則だけと言ってもいいでしょう。（「演繹系とお絵描き圏論」も参照。）
背景となる圏の種類
圏論をベースにするので、古典論理のシーケント計算とは大きく異なる点があります。シーケントの左右におけるカンマの意味は同じです。右側でも左側でもカンマは「∧」（論理AND）の意味です。さらに、論理ANDは圏のモノイド積と解釈します。
以下のような圏を順番に扱います。対応するシーケント計算もそれに従いだんだん複雑になります。
単なる圏のシーケント計算
圏の対象は、命題 A、 B などで表現します。対象Aに対して恒等射があること、2つの射の余域／域が一致すれば結合ができることを、それぞれ公理と推論規則で表します。
---------[id]
A → A
A → B B → C
-----------------[comp]
A → C
単なる圏に対応する公理・推論規則はこれだけです。ホムセットで考えると、この公理・推論規則は次の写像に対応します。
- id : 1→C(A, A)
- comp : C(A, B)×C(B, C)→C(A, C)
モノイド圏のシーケント計算
モノイド圏のシーケント計算*2では、単なる命題（対象）以外に、命題の列 A, B などが登場し、列全体をΓなどで表します。次がモノイド積に対応する推論規則です。
Γ → Δ Φ → Ψ
---------------------[prod]
Γ,Φ → Δ,Ψ
左右のカンマを論理ANDと解釈すれば、論理的推論としても納得がいくものでしょう。
結合は次のように修正します。これは使いやすい推論規則になります。記法を少し工夫すれば、モノイド積の規則と結合の規則を1つにまとめることもできます*3。
Γ → Δ,B B,Φ → Ψ
-------------------------[rcomp]
Γ,Φ → Δ,Ψ
Γ → A,Δ Φ,A → Ψ
-------------------------[lcomp]
Φ,Γ → Ψ,Δ
論理定数Iを導入し、Iに関する公理も入れます。
----------[lunit-elim]
I,A → A
----------[runit-elim]
A,I → A
----------[lunit-intro]
A → I,A
----------[runit-intro]
A → A,I
これらの公理は、構造規則にするなら「Iの増減」となります。一般的な増（Weakening, Thinning）と減（Contraction）はありません。次の証明図は「シーケント左辺へのIの左増」を示すものです。
---------[lunit-elim]
I,A → A A,Γ → Δ (仮定)
---------------------------------[rcomp]
I,A,Γ → Δ
対称モノイド圏のシーケント計算
モノイド圏のシーケント計算に、対称性を表す公理を加えるだけです。
------------[symm]
A,B → B,A
構造規則にするなら「換」（Exchange）となります。A,B,C を C,A,B に置換するには、例えば次の証明図を使います。
------------[symm]
C,B → B,C A,B,C → Δ （仮定）
-------------------------------------[lcomp]
------------[symm]
C,A → A,C A,C,B → Δ
---------------------------------[rcomp]
C,A,B → Δ
デカルト圏のシーケント計算
デカルト圏は、対称モノイド圏に対して対角射と破棄射（discarder, discharger）を追加して定義できます。対角射と破棄射に対応する公理は次のものです。
----------[diag]
A → A,A
--------[disc]
A → I
対角射（コピー）と破棄射（無視）を利用すれば、一般的な減の構造規則（と同等な証明図）を与えることができます。デカルト圏の特徴であるペアリングと射影は次のようになります。
A → B A → C
--------[diag] ----------------[prod]
A → A,A A,A → B,C
-----------------------------[comp]
A → B,C
--------[disc]
A → B,C C → I
------------------[rcomp] ----------[runit-elim]
A → B,I B,I → B
-----------------------------------[comp]
A → B
デカルト閉圏のシーケント計算
いよいよデカルト閉圏です。圏の指数 BA を表すために含意記号「⊃」を導入します。そして、カリー化（ラムダ抽象）Λ:C(A×B, C)→C(A, CB) とカリー化の逆Λ-1に相当する推論規則を定義します。
A,B → C
------------[curry]
A → B⊃C
A → B⊃C
------------[uncurry]
A,B → C
評価射evは公理として導入します。
-------------[ev]
A⊃B,A → B
次の図は、A,B → C と I → A を仮定して、I → B⊃C を導出する証明図です。これは、2引数関数の第1引数を具体値で束縛して、高階関数インスタンスを作る過程の詳細を表現しています*4。
A,B → C
--------- ----------
I,A → A A → B⊃C
---------------------
I,A → B⊃C
---------------
I → A⊃(B⊃C) I → A
----------------------- --------------------
I,I → A⊃(B⊃C),A A⊃(B⊃C),A → B⊃C
-------- ------------------------------------------
I → I,I I,I → B⊃C
-------------------------
I → B⊃C
