判断形式を普通に書く

型理論の人々は「判断形式で書かないと死んでしまう」のでしょうか？ そして、判断形式にターンスタイル（'$`\vdash`$'）とコロン（'$`:`$'）以外使ったら死んでしまう」のでしょうか？

ターンスタイルとコロンへの執着は、もはや「好みの問題」の域を超えている気がします。明らかに弊害が出る状況なので、もう執着するのはやめたほうがいいだろう、と。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\twoto}{\Rightarrow }
%\newcommand{\op}{\mathrm{op} }
\newcommand{\In}{\text{ in }}
\newcommand{\On}{\text{ on }}
\newcommand{\id}{\mathrm{id}}
%\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
%\newcommand{\hyp}{ \text{－} }
\newcommand{\Iff}{ \Leftrightarrow }
%\newcommand{\Imp}{ \Rightarrow }
\newcommand{\Rule}{\rightrightarrows}
`$

内容：

コラリア／ディ-リベールティの判断的セオリー

コラリア／ディ-リベールティの次の論文をチラ見・拾い読みしました。

• [CL21-24]
• Title: Context, Judgement, Deduction
• Authors: Greta Coraglia, Ivan Di Liberti
• Submitted: 17 Nov 2021 (v1), 1 Nov 2024 (v3)
• Pages: 61p
• URL: http://arxiv.org/abs/2111.09438

次の動画もあります。

• https://www.youtube.com/watch?v=lfm8HH5gLyU (2022/01/15)

コラリア／ディ-リベールティは、圏論的構造として判断的セオリー〈judgemental theory〉を定義して、それに対応する形式的計算システムとして判断計算〈judgement calculus〉も定義しています。判断計算は、判断と規則からなりますが、判断と規則の構文形式は、できるだけ伝統的な形式に合わせようとしています。

伝統的な形式に合わせる必要ってあるのかな？ いや、事情は分かるんですけどね。既存の型理論との関係性をアピールするには、既存の構文形式への翻訳を提供すれば「なるほどね」となりますからね。

しかし、伝統や習慣のしがらみを外して考えた場合、判断計算の構文形式として既存の構文形式が良いものか？ と言うと、そうとは思えません。むしろ、悪い選択に思えます。圏論的構造を記述するなら、普通の圏論の言葉や記法を使えばいいんじゃないの。

普通に書いたほうがいいと思う理由はまだあります。比較的最近、次の型理論の判断形式〈judgement form〉の解釈で混乱してしまいました。

$`\quad \Gamma \vdash a : A`$

混乱の原因は、違った解釈を同じ形式で書くことでした。圏論の普通の書き方で書くなら：

1. $`a : \mbf{1} \to A \In \pi^{-1}(\Gamma)`$ （$`\pi^{-1}`$ はファイブレーションの射影の逆像）
2. $`\mrm{ty}(a) = A \In \pi^{-1}(\Gamma)`$ （$`\mrm{ty}`$ はインスタンス項への型の割り当て）

意味が違うのに、なんで同じ判断形式で書くのでしょうか？ 僕にはちょっと理解できません。なので、冒頭に書いたごとくに「そうしないと死んでしまう人々なのだろう」としか思えません。

型理論の判断形式を使うと、非常に簡潔に書けます。しかし、簡潔さの代償として、多くの情報を暗黙化します。コラリア／ディ-リベールティも簡潔な記述を目指しているので、えげつない「記号の乱用、短縮記法、完全な省略」を使っています。その記法は簡潔さ（≒難読さ）の極北とも言えるものです。

なんでそこまで簡潔にしないといけないの？ そうしないと死んでしまうの？

圏論の普通の書き方

要素の集合への所属関係の記号 '$`\in`$' は、集合論起源の記号です。圏に対してもそのまま $`A\in \cat{C}`$ のように使うこともありますが、ここでは、圏論的命題では $`\In`$ を使います。等式が集合 $`X`$ 上で成立することを明示するには $`\On X`$ を添えます。

$`\text{圏論的記法}`$	$`\text{集合論的記法}`$
$`A \In \cat{C}`$	$`A \in |\cat{C}|`$
$`f:A\to B \In \cat{C}`$	$`f \in \cat{C}(A, B)`$
$`A = B \In \cat{C}`$	$`A = B \On |\cat{C}|`$
$`f = g :A \to B \In \cat{C}`$	$`f = g \On \cat{C}(A, B)`$

ここで使っているコロン（'$`:`$'）と矢印（'$`\to`$'）は、型理論や論理で使う意味合いは一切ありません（「記号のグリフと使用場面・使用意図： 型理論、圏論、集合論、論理など」参照）。

ファイバーへの制限と依存ペア

型理論や論理との連絡をよくするために、注釈を下付きにした縦棒記号 $`\mid_{\cdots}`$ を導入します。縦棒記号の使い途は二つあり、ファイバーへの制限と依存ペアを書くために使います。

$`F:\cat{C}\to \cat{Z}`$ を関手として、$`X\in |\cat{Z}|`$ に対して、$`F^{-1}(X)`$ を逆像達が作る部分圏だとします。具体的には：

• 対象集合〈set of objects〉： $`|F^{-1}(X)| := \{A\in |\cat{C}|\mid F(A) = X\}`$
• 射集合〈set of morphisms〉： $`\mrm{Mor}(F^{-1}(X)) := \{f\in \mrm{Mor}(\cat{C})\mid F(f) = \id_X\}`$

$`F^{-1}(X)`$ は $`\cat{C}`$ の部分圏になります。$`F^{-1}(X)`$ を、$`X`$ 上の $`F`$ のファイバー〈fiber〉とも呼びます。なお、$`F`$ は関手ならなんでもよくて、ファイブレーション（の射影）である必要はありません。

$`X\mid_F\; \cdots`$ と書くと、圏論の命題を $`X`$ 上のファイバーに制限することにします。

$`\text{縦棒付き圏論的記法}`$	$`\text{集合論的記法}`$
$`X\mid_F A \In \cat{C}`$	$`A \in |F^{-1}(X)|`$
$`X\mid_F f:A\to B \In \cat{C}`$	$`f \in F^{-1}(X)(A, B)`$
$`X\mid_F A = B \In \cat{C}`$	$`A = B \On |F^{-1}(X)|`$
$`X\mid_F f = g :A \to B \In \cat{C}`$	$`f = g \On F^{-1}(X)(A, B)`$

ファイブレーションはもちろん、単なる関手に対しても使えます。

次に、依存ペア $`(X \mid_F A)`$ です。これは、圏 $`\cat{C}`$ の要素を表します。実際のところ、次の意味です。

$`\quad (X \mid_F A) = A`$

しかし、$`F`$ と $`X`$ に関して次が成立しています。

$`\quad F(A) = X`$

図式で書けば次のようです。

$`\quad \xymatrix{
{(X\mid_F A) \in |\cat{C}|}
\ar@{|->}[d]
\\
{X \in |\cat{Z}|}
}
`$

$`(X\mid_F A)`$ は、$`X`$ 上の $`F`$ のファイバー内に居る $`A`$ ということです。

多くの場合、関手 $`F`$ は固定しているか、文脈から容易に推測できるので、下付きの $`F`$ は省略します。

伝統的判断形式を普通に書くと

型理論に出てくる典型的かつ多数派の判断形式を3つ挙げます。

1. $`\Gamma \vdash`$
2. $`\Gamma \vdash A`$
3. $`\Gamma \vdash a:A`$

まず次の状況で考えます。

$`\quad \pi : \mbf{Type} \to \mbf{Ctx} \In \mbf{CAT}`$

$`\pi`$ はファイブレーションになっていて、ファイバー $`\pi^{-1}(\Gamma)`$ は終対象 $`\mbf{1} = (\Gamma \mid \mbf{1})`$ を持つ圏だとします。

$`\text{型理論的記法}`$	$`\text{縦棒付き圏論的記法}`$
$`\Gamma \vdash`$	$`\Gamma \In \mbf{Ctx}`$
$`\Gamma \vdash A`$	$`\Gamma \mid A \In \mbf{Type}`$
$`\Gamma \vdash a:A`$	$`\Gamma \mid a: \mbf{1}\to A \In \mbf{Type}`$

別な状況設定にします。

$`\quad \xymatrix{
\mbf{Term} \ar[rr]^{\mrm{ty}} \ar[dr]_{\pi_{\mbf{Term}}}
&{}
&{\mbf{Type}} \ar[dl]^{\pi^{\mbf{Type}}}
\\
{}
&{\mbf{Ctx}}
&{}
}\\
\quad \text{commutative }\In \mbf{CAT}
`$

下付きの $`\pi_{\mbf{Term}}`$ と $`\pi_{\mbf{Type}}`$ は、文脈から分かるので省略します。

$`\text{型理論的記法}`$	$`\text{縦棒付き圏論的記法}`$
$`\Gamma \vdash`$	$`\Gamma \In \mbf{Ctx}`$
$`\Gamma \vdash A`$	$`\Gamma \mid A \In \mbf{Type}`$
$`\Gamma \vdash a:A`$	$`\Gamma \mid \mrm{ty}(a) = A \In \mbf{Type}`$

ファイバー積の例

関手 $`F:\cat{C}\to \cat{Z}`$ と $`G:\cat{D}\to \cat{Z}`$ のファイバー積（コスパンの極限対象）を $`(\cat{C}, F)\times (\cat{D}, G)`$ と書きます。これは、ヴォエヴォドスキーが使っていた、中途半端な省略や略記をしない記法です（「ん？ ファイバー積はそれほど簡単じゃないよ」参照）。プルバック四角形の対角線になる関手を $`F\triangledown G`$ と書くことにします。

$`\quad \xymatrix{
{(\cat{C}, F)\times (\cat{D}, G)} \ar[r] \ar[d]
\ar[dr]|{F\triangledown G}
&{\cat{D}} \ar[d]^G
\\
{\cat{C}} \ar[r]_{F}
&{\cat{Z}}
}\\
\quad \quad \text{pullback }\In \mbf{CAT}
`$

特定の対象 $`X\in |\cat{Z}|`$ に対して、関手 $`F\triangledown G`$ によるファイバーがどうなるか（の一部）を規則（型理論や論理における命題と規則： 混同する事情）として記述すると次のようです。

$`\quad (X\mid A) \In \cat{C}\\
\quad (X\mid B) \In \cat{D}\\
\Rule\\
\quad (X\mid A, B) \In (\cat{C}, F)\times(\cat{D}, G)
`$

ここで、依存リスト $`(X\mid A, B)`$ は、ファイバー積 $`(\cat{C}, F)\times (\cat{D}, G)`$ の対象を表します。

ファイバーへの制限を表わす縦棒を使って書きましょう。今度は、縦棒の下付き注釈を書くことにします。

$`\quad X\mid_F A \In \cat{C}\\
\quad X \mid_G B \In \cat{D}\\
\Rule\\
\quad X\mid_{F\triangledown G} (A, B) \In (\cat{C}, F)\times(\cat{D}, G)
`$

おわりに

普通の圏論の記法に、ファイバーへの制限と依存ペア／依存リストの記法を付け足せば、判断形式を使った記述は問題なく書けると思います、ずっとわかりやすく。図式を併用すれば（図式を使った定義や記述）さらにわかりやすいです。

簡潔な記法を使えば、計算が素早くなるのはそのとおりです。が、それは速記用の特別な記法として使えばいいわけで、通常用途では普通の圏論の記法（と図式）で十分ではないでしょうか。

[追記]
コロン、ターンスタイル、カンマを無闇と使うのはやめてくれー、という話は以前にも書いてました。

• 型理論のコロン、ターンスタイル、カンマ

「記号のグリフと使用場面・使用意図： 型理論、圏論、集合論、論理など」では：

僕の個人的感想としては、型理論独自の記法をやめて、圏論と集合論の記法で書き換えてしまえばスッキリすると思うのですが ‥‥

と書いてますが、この記事はスッキリさせる試みの一環です。
[/追記]