このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

最近の型理論: 型判断/シーケントの意味論に向けて

依存型理論で述語論理が出来てしまう理由」において、2つの圏をもとにしてハイパードクトリンを構成する方法の概略を示しました。このハイパードクトリンは、依存型理論と述語論理のどちらも記述できる汎用的な機構になっています。

銀河(型をホストする圏)からハイパードクトリンを構成したい動機のひとつは、構文的に定義される“型理論の型判断”や、“論理のシーケント”にハッキリした意味を与えたいからです。「ハッキリした意味」の“意味”をこの記事で説明します。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\J}{\mathrm{J}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\In}{\text{ in }}
\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\hyp}{ \text{-} }
\newcommand{\twoto}{\Rightarrow }
`$

内容:

シリーズ・ハブ記事:

基本概念

依存型理論で述語論理が出来てしまう理由」で導入した概念を手短に復習します。記号 $`U, \cat{C}, \cat{D}, \cat{P}`$ は、次のような意味だとします。

  • $`U`$ : グロタンディーク宇宙。$`{\bf Set}, {\bf SET}, {\bf Cat}, {\bf CAT}`$ などは、$`U`$ に対して相対的に定義されるとします。
  • $`\cat{C}, \cat{D}`$ : $`U`$-局所小なデカルト圏(小さいデカルト圏なら、もちろんOK)。$`\cat{D}`$ は$`\cat{C}`$-両完備だとします。
  • $`\cat{P}`$ : $`\cat{P}[\hyp] := {\bf CAT}(\J(\hyp), \cat{D})`$ として定義される、デカルト圏 $`\cat{C}`$ 上のインデックス付き圏(圏値の反変関手)。$`\J:\cat{C} \to {\bf CAT}`$ は型圏化関手です。

$`\cat{P}`$ は $`\cat{C}, \cat{D}`$ から一意的に決まってしまうので、$`\cat{C}, \cat{D}, \cat{P}`$ は独立ではありません。

述語論理: 二重圏的ハイパードクトリン」において、シード射シード四角形という概念を導入しました。シード射/シード四角形は、インデックス付き圏 $`\cat{P}`$ がハイパードクトリンになる条件(以下の2つ)を記述する目的で導入したものです。

  1. $`f:A \to B \In \cat{C}`$ がシード射であれば、$`\cat{P}[f] : \cat{P}[B] \to \cat{P}[A] \In {\bf CAT}`$ は左随伴関手と右随伴関手を持ち、2つの随伴系〈随伴トリプル系〉を作れる。
  2. シード四角形に関しては、$`\cat{P}`$ とその随伴系がベック/シュバレー条件を満たす。

述語論理: 二重圏的ハイパードクトリン」では、シード射の全体が $`\cat{C}`$ の部分圏となることを要求してますが、とりあえずは射のクラス($`\mrm{Mor}(\cat{C})`$ の部分集合)でもよさそうです。当面、デカルト圏の射影がシード射であり、シード四角形は次の形の引き戻し〈プルバック〉四角形です*1

$`\require{AMScd}
\begin{CD}
X\times Y @>{t \times \id_Y}>> X'\times Y\\
@VV{\pi_{X, Y}}V @VV{\pi_{X', Y}}V\\
X @>{t}>> X'
\end{CD}\\
\text{pullback in }\cat{C}
`$

圏 $`\cat{C}`$ にシード射/シード四角形(のクラス)が指定されてないと、$`\cat{C}`$ 上のインデックス付き圏 $`\cat{P}`$ がハイパードクトリンである条件が記述できないのです。デカルト圏に関しては、射影と引き戻し四角形が具体的かつ典型的なシード射/シード四角形を与えています。

記法について少し

この記事内で必要なわけでもないのですが、引き続くシリーズ記事から参照する目的で、ハイパードクトリンに関する記法も(変更点も含めて)手短にまとめておきます。

圏論的述語論理とお絵描き」では、"A Taste of Categorical Logic — Tutorial Notes" に倣って、全称限量子に相当するコンビネータ(ホムセットのあいだの写像、「射ファミリーと圏論的コンビネータ」参照)を $`\forall^X_T(p)`$ のように書いてました。ここで重要なのは $`X`$ なので $`T`$ を省略すると $`\forall^X(p)`$ 、これは他の記法と整合性がないなー、と思ったので、
$`\quad {^T \forall_X}(p)`$
または、
$`\quad {^T \forall}X.p`$
に変更します。ほとんどの場合、左肩の $`T`$ は省略されます。述語論理の場合、$`T`$ は背景論域〈background domain of discourse〉、$`X`$ が限量〈量化〉〈quantification〉の範囲となるローカルな論域〈{local | current} domain of discourse〉です。

直積の第一射影の書き方は $`\pi_1^{T, X}`$ だったり $`\pi^1_{T, X}`$ だったり(個人的にも世間的にも)安定しませんが、まー、別にどっちでもいいでしょう。今回は $`\pi_1^{X, Y}`$ で、略記して $`\pi^{X, Y}`$ とします(気分)。

先の全称限量子記法は、より一般的な $`\forall_f`$ の特殊ケースで:

$`\quad {^T \forall_X}(p) := \forall_{\pi^{T, X}}(p)`$

$`\forall_f`$ も、右カン拡張の別記法として定義します。まとめると、次の表です。

$`\text{依存型理論}`$ $`\text{述語論理}`$ $`\text{圏論}`$
$`\Sigma_f`$ $`\exists_f`$ $`\mrm{Lan}_{\J(f)}`$
$`\Delta_f`$ $`\diamondsuit_f`$ $`\mrm{Can}_{\J(f)}`$
$`\Pi_f`$ $`\forall_f`$ $`\mrm{Ran}_{\J(f)}`$

幾つか注意事項:

  1. $`\diamondsuit_f`$ は、構文的には述語の変数を水増しするコンビネータです。ダイアモンド記号は一般的な記法ではありません。
  2. $`\mrm{Can}_K`$ は、関手 $`K`$ をプレ結合して関手を引き戻すコンビネータです。Left と Right の真ん中にあるので Center のつもりですが、「カン」と発音できます。これも一般的な記法ではありません。僕が考えた駄洒落です。
  3. $`\J`$ は型圏化関手で、デカルト圏の射を渡すと関手にします。

今回この記事では述語論理風の記法を使いますが、それは記法だけの話で、依存型理論の場合にも通用します。依存型理論の概念も述語論理の概念も、同じ方法で(カン拡張により)定式化できることは以下の3つの過去記事に書いています。

意味的シーケント

インデックス付き圏 $`\cat{P}`$ からグロタンディーク構成した平坦化圏〈flattened category〉を $`\int_\cat{C} \cat{P}[\hyp]`$ 、あるいはより短く $`\int \cat{P}`$ と書くことにします。$`X\in |\cat{C}|`$ と $`p\in |\cat{P}[X]|`$ のペア $`(X, p)`$ が平坦化圏 $`\int \cat{P}`$ の対象となります。次の形の射は、ひとつのファイバー内に収まる“垂直な射”なので、ファイバー射〈{fiber | fibre} morphism〉と呼びます。

$`\quad \varphi : (X, p) \to (X, q) \In \int \cat{P}`$

述語論理の場合は、ファイバー射は同じ論域上の述語命題のあいだの証明になります。ファイバー射は、次の形の射でもあります。

$`\quad \varphi : p \to q \In \cat{P}[X]`$

ファイバー射のプロファイル(域と余域の指定)を次のようにも書きます。

$`\quad X, p \overset{\varphi}{\to} q`$ ($`\cat{P}`$ は暗黙に前提する)

この形に書いたプロファイルを意味的シーケント〈semantic sequent〉と呼びます。意味的シーケントは、インデックス付き圏におけるプロファイルの別記法に過ぎません。通常の圏論における非形式的命題(地の文)です。形式的構文としての定義は何もしてません

次の3つの書き方は同じ意味です。

  1. $`\varphi : (X, p) \to (X, q) \In \int \cat{P}`$
  2. $`X, p \overset{\varphi}{\to} q`$ ($`\cat{P}`$ は暗黙に前提する)
  3. $`\varphi \in \cat{P}[X](p, q)`$

形式的構文として定義されたシーケントや型判断の意味は、意味的シーケントとして記述します(その心積もりです)。が、大域コンテキスト〈global context〉を持った型判断の記述などには、次の形の意味的シーケントもあったほうが便利です。以下の '$`\|`$' が大域コンテキストとローカルコンテキストの区切りになります。

$`\quad T, u \| X, p \overset{\varphi}{\to} q`$

この「意味的シーケント」の“意味”は次節以降で説明します。

環境・前提付き計算

$`\cat{E}`$ をデカルト圏だとして、$`\cat{E} = (\cat{E}, \land, \top)`$ と書きます。記号は論理ANDと論理Trueを使ってますが、別に論理的文脈でなくてもかまいません。$`\cat{E}`$ の対象をラテン文字小文字で書きますが、特段の理由はありません。

対象 $`w\in |\cat{E}|`$ をひとつ選んで固定します。$`\cat{E}`$ と $`w`$ から、新しい圏 $`\cat{E}_{(w\land)}`$ を定義しましょう。

  • $`|\cat{E}_{(w\land)}| = |\cat{E}|`$
  • $`\cat{E}_{(w\land)}(p, q) := \cat{E}(w\land p, q)`$

$`\cat{E}_{(w\land)}`$ における射の結合 $`;;`$ は次のようにします。$`\Delta`$ はデカルト圏 $`\cat{E}`$ の対角射〈コピー射〉、$`\alpha`$ はデカルト積の結合律子〈associator〉です。

$`\text{For }\varphi \in \cat{E}_{(w\land)}(p, q), \psi\in \cat{E}_{(w\land)}(q, r)\\
\quad \varphi ;; \psi := (\Delta_w \land \id_p); \alpha_{w, w, p} ; (\id_w \land \varphi) ; \psi : w\land p \to r \In \cat{E}`$

$`\cat{E}_{(w\land)}`$ における恒等射 $`\id'`$ は次です。$`!`$ はデカルト圏 $`\cat{E}`$ の終射〈破棄射〉、$`\lambda`$ は左単位律子〈left unitor〉です。

$`\text{For }p \in |\cat{E}_{(w\land)}|\\
\quad \id'_p := (!_w \land \id_p); \lambda_p : w\land p \to p \In \cat{E}`$

この定義により、$`\cat{E}_{(w\land)}`$ が圏になることは確認できます。定義に使った $`;;,\, \id'`$ は、通常の $`;,\, \id`$ に変えて、オーバーロードして使います。なお、$`\cat{E}_{(w\land)}`$ は、コモナドの余クライスリ圏としても定義できます(次節で説明)。もし $`\cat{E}`$ がデカルト閉圏なら、カリー化を使ってコモナドをモナドに変換して $`\cat{E}_{(w\land)}`$ と事実上同じ圏をクライスリ圏として定義できます。

対象に対するデカルト積をもとのままに保存して、デカルト積を $`\cat{E}_{(w\land)}`$ まで持ち上げることができます。これは、細かい計算を実行すれば分かります。ストリング図を使って計算するのがオススメです。

結局、$`\cat{E}, w \mapsto \cat{E}_{(w\land)}`$ という構成は、デカルト圏からデカルト圏を作り出します。$`\psi :v \to w \In \cat{E}`$ があると、デカルト圏のあいだの関手*2 $`\cat{E}_{(w\land)} \to \cat{E}_{(v\land)}`$ を構成できます。全体として次のような関手(インデックス付き圏)になります。

$`\quad \cat{E}_{(\hyp \land)} : \cat{E}^\mrm{op} \to {\bf CartCAT}`$

ここで、$`{\bf CartCAT}`$ は“デカルト圏の圏”です。

$`\cat{E}_{(w\land)}`$ の射は、対象 $`w`$ を大域環境(ラムダ計算の場合)、または大域前提(論理の場合)として持つ射です。よって、デカルト圏 $`\cat{E}_{(w\land)}`$ は、環境(または前提)が付いた計算(または証明)を扱う計算系になります。

コモノイド・コスタンピング構成

モノイド圏上のモナド/コモナドの話をちょっとします。$`\cat{C} = (\cat{C}, \otimes, I)`$ をモノイド圏とします。

$`(M, m, e)`$ をモノイド圏 $`\cat{C}`$ のモノイド対象(以下、単にモノイド)とします。モノイドの台対象 $`M`$ をモノイド積の意味で掛け算する自己関手 $`\hyp\otimes M`$ (左からの掛け算でもよい)から、モノイド乗法とモノイド単位を使って $`\cat{C}`$ 上のモナド $`(\hyp\otimes M, \mu, \eta)`$ を作れます。この方法で作られたモナドはモノイド・スタンピング・モナド〈monoidal stamping monad〉と呼びます。

$`(D, d, i)`$ をモノイド圏 $`\cat{C}`$ のコモノイド対象(以下、単にコモノイド)とします。コモノイドの台対象 $`D`$ をモノイド積の意味で掛け算する自己関手 $`D \otimes \hyp`$ (右からの掛け算でもよい)から、コモノイド余乗法とコモノイド余単位を使って $`\cat{C}`$ 上のコモナド $`(D\otimes\hyp , \delta, \iota)`$ を作れます。この方法で作られたコモナドはコモノイド・コスタンピング・コモナド〈comonoidal costamping comonad〉と呼びます。

$`\cat{C}`$ がデカルト圏〈デカルト・モノイド圏〉の場合、任意の対象が、対角射〈コピー射〉と終射〈破棄射〉を使って自動的・標準的にコモノイドになります。このコモノイドを $`(A, \Delta_A, !_A)`$ のように書きます。前節の $`\cat{E}_{(w\land)}`$ は、$`\cat{E}`$ 内のコモノイド $`(w, \Delta_w, !_w)`$ によるコモノイド・コスタンピング・コモナドの余クライスリ圏でした。

圏と、1個の対象を指定した構造 $`(\cat{C}, W)`$ をマーク付き圏〈marked category〉と呼ぶことにします。pointed set にあわせて pointed category と呼びたいところですが、pointed category は別な意味で既に使われています。デカルト圏に1個の対象を指定した場合はマーク付きデカルト圏〈marked cartesian category〉と呼びます。

マーク付きデカルト圏とマーク(指定した対象)を保存するデカルト関手からなる圏を $`{\bf MarkedCartCAT}`$ とします。マーク付き圏 $`(\cat{C}, W)`$ から、コモノイド $`(W, \Delta_W, !_W)`$ によるコモノイド・コスタンピング・コモナドの余クライスリ圏を作る構成は、マーク保存関手と整合して、次の関手(Comonoid Costamping Comonad coKleisli Category)を定義します。

$`\quad \mrm{CCCCC}: {\bf MarkedCartCAT} \to {\bf CartCAT}`$

「マーク保存関手と整合して」とは、デカルト関手 $`F:\cat{C} \to \cat{C'}`$ がマーク $`W`$ をマーク $`W'`$ に移すとき、次のデカルト関手が上手く作れるということです。

$`\quad \mrm{CCCCC}(F) : \mrm{CCCCC}(\cat{C}, W) \to \mrm{CCCCC}(\cat{C'}, W') \In {\bf CartCAT}`$

厳密デカルト圏と厳密デカルト関手のケースで考えるとほぼ明らかですが、厳密でない(等式法則が成立しない)場合は、細かい議論が面倒になります。今は面倒なことをしたくないので、細かい議論を省略して、$`\mrm{CCCCC}(F)`$ が定義可能だという事実を利用します。なお、$`\mrm{CCCCC}(F)`$ は長すぎるので、$`\widetilde{F}_{W,W'}`$ を使います。下付きの $`W, W'`$ は、$`F`$ でマークが保存されることを意味します。

デカルト・インデックス付き圏の変形 1

$`\cat{P}: \cat{C}^\mrm{op} \to {\bf CAT}`$ はハイパードクトリンのインデックス付き圏ですが、ここからの話は、ハイパードクトリンの随伴トリプルとは無関係です。次の条件を満たすインデックス付き圏 $`\cat{P}`$ に対して通用する話です。

  1. インデックス付き圏 $`\cat{P}`$ のベース圏 $`\cat{C}`$ はデカルト圏である。
  2. すべての $`A\in |\cat{C}|`$ に対して、$`\cat{P}[A]`$ はデカルト圏である。
  3. すべての $`f:A \to B \In \cat{C}`$ に対して、$`\cat{P}[f]`$ はデカルト圏のあいだのデカルト構造を保つ関手である。

つまり、すべての登場人物がデカルト〈cartesian〉であるインデックス付き圏です。このようなインデックス付き圏をデカルト・インデックス付き圏〈cartesian indexed category〉と呼ぶことにします。

「環境・前提付き計算」の節で出てきた $`\cat{E}_{(\hyp\land)}`$ はデカルト・インデックス付き圏の事例です。$`\cat{F}[\hyp] := \cat{E}_{(\hyp\land)}`$ と置くと、

$`\quad \cat{F}:\cat{E}^\mrm{op} \to {\bf CAT}`$ (インデックス付き圏)

であり:

  1. インデックス付き圏 $`\cat{F}`$ のベース圏 $`\cat{E}`$ はデカルト圏である。
  2. すべての $`w\in |\cat{E}|`$ に対して、$`\cat{F}[w]`$ はデカルト圏である。
  3. すべての $`\psi:v \to w \In \cat{E}`$ に対して、$`\cat{F}[\psi]`$ はデカルト圏のあいだのデカルト構造を保つ関手である。

与えられたデカルト・インデックス付き圏 $`\cat{P} : \cat{C}^\mrm{op} \to {\bf CartCAT}`$ を、$`T\in |\cat{C}|`$ を使って変形します。変形したインデックス付き圏を $`\cat{P}_{T}`$ と書きます。

  • $`X\in |\cat{C}|`$ に対して、$`\cat{P}_T[X] := \cat{P}[T \times X] \in |{\bf CartCAT}|`$
  • $`f:A \to B \In \cat{C}`$ に対して、
    $`\quad \cat{P}_T[f] := (\cat{P}[T \times f] : \cat{P}[T \times B] \to \cat{P}[T \times A] \In {\bf CartCAT})`$

上に出てきた $`T \times f`$ という書き方は $`\id_T \times f`$ のことです(よく使われる書き方です)。上記の定義により、新しいデカルト・インデックス付き圏 $`\cat{P}_T : \cat{C}^\mrm{op} \to {\bf CartCAT}`$ が決まります。$`\cat{P}_T`$ が実際にデカルト・インデックス付き圏になること(デカルト・インデックス付き圏の条件を満たすこと)は次のように確認できます。

  1. インデックス付き圏 $`\cat{P}_T`$ のベース圏 $`\cat{C}`$ はデカルト圏である。($`\cat{P}`$ のベース圏と同じだから。)
  2. すべての $`A\in |\cat{C}|`$ に対して、$`\cat{P}_T[A] = \cat{P}[T\times A]`$ はデカルト圏である。($`\cat{P}`$ の性質から。)
  3. すべての $`f:A \to B \In \cat{C}`$ に対して、$`\cat{P}_T[f] = \cat{P}[T \times f]`$ はデカルト圏のあいだのデカルト構造を保つ関手である。($`\cat{P}`$ の性質から。)

$`g:S \to T \In \cat{C}`$ があると、次のような自然変換を定義できます*3

$`\quad \tau_g :: \cat{P}_T \twoto\cat{P}_S : \cat{C}^\mrm{op} \to {\bf CartCAT}`$

自然変換 $`\tau_g`$ の成分は、各対象 $`X\in |\cat{C}|`$ ごとの成分である $`{\bf CartCAT}`$ の1-射、つまり関手を割り当てれば定義できます。

$`\quad (\tau_g)_X := \cat{P}[g \times X] : \cat{P}_T[X] \to \cat{P}_S[X] \In {\bf CartCAT}`$

1-射(関手)の族 $`( (\tau_g)_X)_{X\in |\cat{C}|}`$ が自然変換であるためには、 $`h:W\to X \In \cat{C}`$ に対して次の図式が可換になる必要があります。

$`\begin{CD}
\cat{P}_T[X] @>{(\tau_g)_X}>> \cat{P}_S[X]\\
@V{\cat{P}_T[h]}VV @VV{\cat{P}_S[h]}V\\
\cat{P}_T[W] @>{(\tau_g)_W}>> \cat{P}_S[W]\\
\end{CD} \\
\text{ in }{\bf CartCAT}`$

定義によって展開すれば、上の図式は次と同じです。

$`\begin{CD}
\cat{P}[T\times X] @>{\cat{P}[g \times X]}>> \cat{P}[S\times X]\\
@V{\cat{P}[T\times h]}VV @VV{\cat{P}[S\times h]}V\\
\cat{P}[T \times W] @>{\cat{P}[g \times W]}>> \cat{P}[S\times W]\\
\end{CD} \\
\text{ in }{\bf CartCAT}`$

$`\cat{P}[\hyp]`$ が、圏の結合演算とデカルト積演算を保つのであれば、$`\cat{C}`$ における交替律(下)から上記図式の可換性を導けます*4

$`\quad (g \times X);(S \times h) = (T\times h);(g \times W) = g\times h \;\In \cat{C}`$

以上により、$`g: S \to T \In \cat{C}`$ が自然変換 $`\tau_g :: \cat{P}_T \twoto \cat{P}_S`$ を誘導することが分かりました。自然変換は関手圏の1-射なので、

$`\text{For } g: S \to T \In \cat{C}\\
\quad \tau_g : \cat{P}_T \to \cat{P}_S \In [\cat{C}^\mrm{op}, {\bf CartCAT}]`$

諸々の条件を確認すると、次のような関手 $`\cat{P}^\clubsuit`$ が定義できることが分かります。

  • $`\cat{P}^\clubsuit : \cat{C}^\mrm{op} \to [\cat{C}^\mrm{op}, {\bf CartCAT}]`$
  • $`\cat{P}^\clubsuit(T) := \cat{P}_T`$
  • $`\cat{P}^\clubsuit(g) := \tau_g`$

この関手 $`\cat{P}^\clubsuit`$ は、反変・反変の二項関手 $`\cat{P}[\hyp \times \hyp]`$ のカリー化になっています。このことを示すには、「モノイド圏と加群圏に関するフォークロアとマックレーン五角形・三角形」で述べた一般論を利用できます。

デカルト・インデックス付き圏の変形 2

デカルト・インデックス付き圏 $`\cat{P}: \cat{C} \to {\bf CartCAT}`$ と $`T \in |\cat{C}|`$ に対して、変形したデカルト:インデックス付き圏 $`\cat{P}_T: \cat{C} \to {\bf CartCAT}`$ が定義できました(前節)。さらに、$`u \in |\cat{P}[T]|`$ を使って変形します。変形のパラメータとなるペア $`(T, u) \text{ where }u\in |\cat{P}[T]|`$ は、デカルト・インデックス付き圏 $`\cat{P}`$ のグロタンディーク平坦化圏 $`\int \cat{P}`$ の対象とみなすとよいでしょう。

定義の前に準備をします。$`\pi^{T, X}: T\times X \to T \In \cat{C}`$ は第一射影です。この第一射影を反変関手である $`\cat{P}[\hyp]`$ に渡すと、$`\cat{P}[\pi^{T, X}] : \cat{P}[T] \to \cat{P}[T\times X] \In {\bf CartCAT}`$ が得られます。$`u\in | \cat{P}[T] |`$ だったので、$`\cat{P}[\pi^{T, X}](u) \in |\cat{P}[T\times X]|`$ です。

もともと $`T`$ 上のファイバー内に居た $`u`$ を射影に反変な“ファイバー間の移動”で $`T\times X`$ 上に移したモノが $`\cat{P}[\pi^{T, X}](u)`$ です。居場所を下付きアットマークで表すことにして:

  • $`u_{@T} := u`$
  • $`u_{@(T\times X)} := \cat{P}[\pi^{T, X}](u)`$

と書くことにします。

次に、マーク付きデカルト圏とマーク保存デカルト関手について見ておきます。まず、次の可換図式があります。

$`\begin{CD}
T \times A @>{T\times f}>> T\times B\\
@V{\pi^{T, A}}VV @VV{\pi^{T, B}}V\\
T @= T
\end{CD}\\
\text{commutative in }\cat{C}`$

これを、反変関手 $`\cat{P}[\hyp]`$ で移します。マークも付けます。

$`\begin{CD}
(\cat{P}[T \times A], u_{@(T\times A)}) @<{\cat{P}[T\times f]}<< (\cat{P}[T\times B], u_{@(T\times B)} )\\
@A{\cat{P}[\pi^{T, A}]}AA @AA{\cat{P}[\pi^{T, B}]}A\\
(\cat{P}[T] ,u) @= (\cat{P}[T], u)
\end{CD}\\
\text{commutative in }{\bf MarkedCartCAT}`$

$`\cat{P}[T\times f]`$ がマークを保存することは、自明というと言い過ぎかも知れませんが、デカルト圏の簡単な計算から出ます。マークを保存する関手はコモノイド・コスタンピング構成に持ち上げることができるので、次のデカルト関手は存在します。

$`\quad \widetilde{\cat{P}[T\times f]}_{u_{@(T\times B)}, u_{@(T\times A)}}:\\
\qquad (\cat{P}[T \times B])_{ ( u_{@(T\times B)}\land)} \to (\cat{P}[T \times A])_{( u_{@(T\times A)} \land)} \In {\bf CartCAT}
`$

さて、準備した素材を使って $`(T, u)\in |\int \cat{P}|`$ に対する変形 $`\cat{P}_{T, u}`$ は次のように定義します。

  • $`X\in |\cat{C}|`$ に対して、$`\cat{P}_{T, u}[X] := (\cat{P}[T \times X])_{(u_{@(T\times X)}\land)} \in |{\bf CartCAT}|`$
  • $`f:A \to B \In \cat{C}`$ に対して、
    $`\quad \cat{P}_{T, u}[f] := (\, \widetilde{\cat{P}[T \times f]}_{u_{@(T\times B)}, u_{@(T\times A)}} : (\cat{P}[T \times B])_{ ( u_{@(T\times B)}\land)} \to (\cat{P}[T \times A])_{( u_{@(T\times A)} \land)} \In {\bf CartCAT} \,)`$

得られた $`\cat{P}_{T, u}`$ がちゃんとデカルト・インデックス付き圏になっていることは確認が必要です。

意味的シーケントの意味

荒っぽい議論もありましたが、一応これで、意味的シーケントの意味論〈セマンティクス〉の準備が出来ました。区切り記号 '$`\|`$' を含む意味的シーケント

$`\quad T, u \| X, p \overset{\varphi}{\to} q`$

は、次の圏論的な非形式的命題(地の文としての主張、メタ命題)の別記法です。

$`\quad \varphi \in \cat{P}_{T, u}[X](p, q)`$

ホムセット $`\cat{P}_{T, u}[X]`$ を定義により展開して書けば:

$`\quad \varphi \in \cat{P}[T\times X](u_{@(T\times X)}\land p, q)`$

$`\cat{P}`$ は、2つのデカルト圏 $`\cat{C}, \cat{D}`$ から決まるのでした。述語論理の文脈なら、 $`\cat{P}`$ は、論域〈domain of discourse〉に“述語からなる論理代数”(「述語論理: ベース圏と論理代数の圏」参照)を対応させるインデックス付き圏になるので、

$`\quad \cat{P} = \mrm{Pred}_\cat{C}^\cat{D}`$

とでも書くのが自然でしょう。この書き方なら、先の意味的シーケントの意味は:

$`\quad \varphi \in \mrm{Pred}_\cat{C}^\cat{D}[T\times X](u_{@(T\times X)}\land p, q)`$

形式的に定義されるシーケント/型判断は、様々な構文を持ちます。それら様々な構文を意味的シーケントにマップすれば、構文によらない議論が出来ます。また、意味を変えない構文のあいだの翻訳を考えることも出来ます。なんにしろ、意味的対象物〈semantic object〉を準備しておく必要はあるのです。

*1:四角形のなかの $`t`$ は、ベースチェンジ射と呼ばれます。が、「ベース」が多用され過ぎなので、述語論理の文脈では背景チェンジ射と呼ぶことにしてます(個人的用法)。

*2:デカルト圏=デカルト・モノイド圏 として、タイトな(構造射が可逆な)モノイド関手とみなすのがよいでしょう。

*3:$`\tau_g`$ が棲んでいる世界が2-圏 $`\mathbb{CAT}`$ なのか3-圏 $`\mathbb{2CAT}`$ なのかで議論が変わってきます。ここでは、多少曖昧なままで説明します。

*4:四角形が厳密に可換でなくても、内部が可逆な2-射で埋められるなら実際には十分です。