型理論周辺の用語・記法・説明が混乱誘発的〈confusing〉で、それは僕の長年の悩みの種です。型理論／論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです*1。
最近、包括コンテキスタッド（「型理論とコンテキスタッド： コンテキストフル射」「包括コンテキスタッドに向けて」参照）を使えば、型理論周辺をうまく整理できるのではないかと思っています。しかし、仮にうまく整理できたとして、それでも混乱をまねく要因は取り除けないでしょう。
そもそも、以下に挙げるダイコトミー〈概念の二分法〉による区分けが難しいのです。その難しさが混乱の要因となります。
- 対象物レベルとメタレベル
- 非形式的表現と形式的表現
- 構文論と意味論
- 関手とその値
- 反変関手と共変関手
- 圏とその反対圏
これらの混乱要因を、この記事で説明します。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\mbb}[1]{ \mathbb{#1} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\op}{\mathrm{op} }
\newcommand{\In}{\text{ in }}
\newcommand{\id}{\mathrm{id}}
%\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{ \text{－} }
%\newcommand{\Iff}{ \Leftrightarrow }
%\newcommand{\Imp}{ \Rightarrow }
`$
内容：
ハブ記事：
文字・記号・語などのレベルと形式性
対象物が、実数や群や体やベクトル空間や圏ならば、対象物レベルとメタレベルの混乱はないし、対象物レベルとメタレベルを意識する必要さえありません。対象物は、公理的に定義された構造とその実例で、対象物を語るための言語は自然言語に数式を混ぜたものです。
対象物が形式言語あるいは形式言語を含む形式体系のときには、対象物レベルとメタレベルの明確な区別が必要になります。文字・記号・語などが、対象言語（語るべき対象物である形式言語）のものか、記述言語（対象物を語るために使う言語）のものか紛らわしくなります。特に、ターンスタイル記号 '$`\vdash`$' や二重矢印 '$`\twoto`$' が厄介です。
'$`\vdash`$' や '$`\twoto`$' が対象物〈対象システム〉を語るためのメタレベルにある場合でも、メタレベルの記号を非形式的に使っているか、形式的に使っているかの区別が必要です。「非形式的に使っている」とは、記述言語である自然言語（我々は日本語使用）のなかに混ぜて記号を使っていることです。「形式的に使っている」とは、対象物〈対象システム〉を語るためのメタな形式言語（人工的な言語）があり、その語彙として記号を使っていることです。
例えば、対象システムが自然演繹系であるとき、ターンスタイル記号 '$`\vdash`$' を「証明可能である」という日本語の短縮形として使っているなら非形式的〈informal | インフォーマル〉に使っています。シーケント計算（という形式体系）の区切り記号としてターンスタイル記号を使っているなら形式的〈formal | フォーマル〉に使っています。
構文論的意味論と意味論的意味論
型理論におけるモデルや意味論には注意が必要です。「最近の型理論： 拡張包括構造を持ったインデックス付き圏」に次のような追記をしています。
型理論の意味論の話をします。（[追記]意味論とは言っても、ほんとのセマンティクスと言うよりは、形式体系の構文圏〈syntactic category〉を構成する話なので、広義の構文論内部の狭義の意味論という感じです。[/追記]）
型理論に出てくる圏、C-システム〈C-system〉、ファミリー付き圏〈category with families〉、包括圏〈comprehension category〉などは、型理論の形式システム〈型システム〉の構文構造を抽象的に定式化したものです。多くの場合、型理論の圏論的モデルや圏論的意味論は構文論の内部での話です。しかし、ローヴェア・セオリーの意味論やインスティチューションのモデル関手は構文論の話ではなく、ほんとの意味論の定式化です。
構文論内部の意味論を構文論的意味論〈syntactic semantics〉として区別したほうがいいと思います。そうなると、ほんとの意味論は意味論的意味論〈semantic semantics〉となります。
意味論は、文字・記号・語などにナニカを意味として割り当てますが、文字・記号・語などが非形式的なモノである場合と、形式的なモノである場合があります。これも考慮すると意味論は以下の4種に分類されます。
- 非形式的構文論的意味論 ： (非形式的に使う文字・記号・語など) $`\mapsto`$ (構文論で扱うモノやコト) と割り当てる。
- 形式的構文論的意味論 ： (形式的に使う文字・記号・語など) $`\mapsto`$ (構文論で扱うモノやコト) と割り当てる。
- 非形式的意味論的意味論 ： (非形式的に使う文字・記号・語など) $`\mapsto`$ (構文論では扱わないモノやコト) と割り当てる。
- 形式的意味論的意味論 ： (形式的に使う文字・記号・語など) $`\mapsto`$ (構文論では扱わないモノやコト) と割り当てる。
例えば、'$`\vdash`$' や '$`\twoto`$' の意味・用法を決めるとき、上の4種のどの目的で決めているかをハッキリさせないと混乱を引き起こすでしょう。
関手が値である反変関手・共変関手
「型理論へのファイブレーション的アプローチ： インスタンスとは」で述べたように、多くの圏論的型理論はファイブレーション〈ファイバー付き圏〉を使います。“ファイブレーション-インデックス付き圏”の対応（グロタンディーク対応）があるので、インデックス付き圏〈圏のファミリー〉を使っているとも言えます。
インデックス付き圏は次のような関手（正確には2-関手）です。
$`\quad \cat{F} : \cat{C}^\op \to \mbf{CAT} \In 2\mathbb{CAT}`$
インデックス付き圏と呼ばれる反変関手の値は次のようになります。
$`\text{For }f:A \to B \In \cat{C}\\
\quad \cat{F}(f) : \cat{F}(B) \to \cat{F}(A) \In \mbf{CAT}
`$
特定の射 $`f\in \mrm{Mor}(\cat{C})`$ に対する値がまた関手（2-圏 $`\mbf{CAT}`$ の1-射）です。
関数と関数値の混同がよくあることなので、関手と関手値の混同もあるでしょう。「値」という曖昧多義な言葉では印象が弱いので「戻り値〈return value〉」を使うことにします。関手戻り値対象〈functor return-value object〉は、関手の戻り値であるところの余域圏の対象のことで、関手戻り値射〈functor return-value morphism〉は、関手の戻り値であるところの余域圏の射となります。
インデックス付き圏 $`\cat{F}`$ の場合は次のようなことになります。
- 関手 $`\cat{F}`$ の関手戻り値対象は圏である。
- 関手 $`\cat{F}`$ の関手戻り値射は関手である。
関手 $`\cat{F}`$ の関手戻り値射である関手 $`\cat{F}(f)`$ はもちろん関手 $`\cat{F}`$ とは別物です。インデックス付き圏の用語法では、インデックス付き圏の関手戻り値関手を再インデキシング関手〈reindexing functor〉と呼びます。
インデックス付き圏は反変関手ですが、余インデックス付き圏〈coindexed category〉は次のような共変関手です。
$`\quad \cat{G} : \cat{C} \to \mbf{CAT} \In 2\mathbb{CAT}`$
余インデックス付き圏の関手戻り値関手は余再インデキシング関手〈coreindexing functor〉です。例えば、インスティチューション理論の文関手〈sentence functor〉は共変関手〈余前層〉なので、その関手戻り値射は余再インデキシング関手です。インスティチューション理論内では、余再インデキシング関手を翻訳関手〈translation functor〉と呼んでいます。なお、オリジナルのインスティチューション理論では、余インデックス付き圏が余前層に退化しているので、余再インデキシング関手〈翻訳関手〉も関数〈翻訳関数〉に退化してます。
コンテキスト達の圏と指標達の圏
「指標の圏はコンテキストの圏の反対圏」と「型理論とインスティチューション理論が繋がるぞ！」に書いたように、型理論のコンテキスト達の圏（$`\cat{C}`$ とする）とインスティチューション理論の指標達の圏（$`\cat{S}`$ とする）は互いに反対圏です。同じ圏を表と裏から見てることからしち面倒くさい事になっています。しち面倒くさい状況は、次の過去記事に書いています。
用語がしち面倒くさくなるのは当然ですが、記法でも困ったことが起こります。インスティチューション理論の文関手 $`\mrm{Sen}`$ は共変関手です。オリジナルの文関手の余域は $`\mbf{Set}`$ ですが、$`\mbf{Cat}`$ に拡張しておきます。
$`\quad \mrm{Sen} : \cat{S} \to \mbf{Cat} \In 2\mbf{CAT}`$
関手戻り値関手 $`\mrm{Sen}(f)`$ を多用するので $`f_*`$ と略記したとしましょう。
同じ関手 $`\mrm{Sen}`$ がコンテキスト達の圏の側では反変関手です。
$`\quad \mrm{Sen} : \cat{C}^\op \to \mbf{Cat} \In 2\mbf{CAT}`$
反変関手の関手戻り値関手を $`f_*`$ と書くのは奇妙ですから $`f^*`$ とすべきでしょう。
互いに反対圏である $`\cat{S}`$ と $`\cat{C}`$ を同時に扱うなら、略記も $`f_*`$ と $`f^*`$ の2種類が必要です。ところが、$`f_*`$ と $`f^*`$ をこの意味で使ってしまうと、随伴トリプルの便利な略記（下）とコンフリクト〈かち合い | バッティング〉してしまいます。
$`\quad f_! \dashv f^* \dashv f_*`$
また、インスティチューション理論では、モデル関手（反変関手）の関手戻り値関手であるリダクト関手 $`\mrm{Model}(f)`$ に $`f^*`$ を使いたい（実際に使っている）のですが、これもコンフリクトします。記法 $`f^*, f_*`$ の奪い合いが発生します。
- $`\cat{S}`$ 上の $`\mrm{Model}(f), \mrm{Sen}(f)`$ に使いたい。
- $`\cat{C}`$ 上の $`\mrm{Sen}(f), \mrm{Model}(f)`$ に使いたい。
- $`\cat{C}`$ 上の随伴トリプルに使いたい。
型理論の $`\cat{C}`$ を使った流儀、インスティチューション理論の $`\cat{S}`$ を使った流儀、それぞれにメリットや便利さがあるので、どちらか一方を完全に切り捨てるのも難しい。しかし両方を使っていると、しち面倒くさく混乱しがちとなるのは避けられない。あー、ジレンマ。
*1:これまでも愚痴や指摘や対策は書いてきました。「型理論ってば」、「最近の型理論のハマリ所」、「型理論へのファイブレーション的アプローチ： インスタンスとは // 「インスタンス」を「項」と呼ぶのはやめよう」など。
