色々とハマル。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\In}{\text{ in }}
\newcommand{\op}{ \mathrm{op} } % used
\newcommand{\hyp}{\text{－} } % used
\newcommand{\ILT}{ \triangleleft } % immediately less than
`$
内容：
構文モデル
「モデル」と言うと、構文に対して意味・解釈を与える意味論的モデルを想定することが多いでしょうが、型システムのモデルは意味論的モデルではないことがあります。語彙と文法で定義された形式体系の構文構造を代数的に定式化した代数系のこともモデルと言います。
意味論的ではないモデルは、構文論的モデル〈syntactic model | 構文モデル〉と呼べば区別がつきます。過去記事「型理論的形式体系の構文代数系はファイバー付き依存多圏」では、構文構造を表現した代数系なので、構文代数系〈{syntax | syntactic} algebraic system〉という言葉を使いました。
構文代数系は、具体的な語彙・文法は捨象しているので、構文中立〈syntax neutral〉とか構文非依存〈syntax independent〉とか形容されます。構文代数系は構文非依存な構文モデルです。が、この言い方はちょっと奇妙ですね。記法非依存〈notation independent〉な構文モデルといえば収まりがいいでしょうか。
例えば、カートメル／ヴォエヴォドスキーのC-システムや、ディビエのファミリー付き圏〈category with families | CwF〉は、記法非依存な構文モデル〈構文代数系〉です。記法（具合的な書き方）には依存してませんが、構文構造の定式化になっています。
ややこしいのは、構文モデルが意味論的モデルと解釈されることがあることです。構文モデルがそのまま、あるいは規準的な構成法で意味論的モデルとみなせます。構文モデルから作られた意味論的モデルは項モデル〈term model〉と呼ばれます。項モデルは多くの場合意味論的モデルの圏の始対象になります。
構文論的な手法で具合的に作られた項モデルが、超越的に定義された意味論的モデル達のなかで始対象となることは、項モデルの始対象性〈initiality〉と呼びます。始対象性を示すのは難しいことがあります。
型と項
型理論では、「型」と「項」という言葉が多用されます。この2つの言葉のバランスが悪くて、誤解の原因になりそうです。意味論が圏論的に与えられるとして、次のような言い方が適切だと思います。
| 構文論 | 意味論 |
|---|---|
| 型項 | 型対象 |
| インスタンス項 | インスタンス射 |
実際には次のように使用されています。
| 構文論 | 意味論 |
|---|---|
| 型 | 型 |
| 項 | 項 |
型理論の構文論と意味論の境界線がハッキリしない（構文代数系や項モデルのような存在物がある）ので、全部同じ用語を使うというのもひとつの方針・態度ですが、誤解・混乱のリスクはありますね。
僕は、次のような言い回しを使っています。「{…}?」は省略するかも知れないことを示します。
| 構文論 | 意味論 |
|---|---|
| 型{項}? | 型{対象}? |
| インスタンス{項?} | インスタンス{射}? |
そうはいっても、伝統・習慣を無視しづらいこともあるので、$`\mrm{Ty}`$（Typeの短縮）、$`\mrm{Tm}`$（Termの短縮）は使うことがあります。フルスペルの Type, Term は思い出さずに、単にニ文字の符丁として使います。
組み込みかユーザー定義か
ファミリー付き圏は、典型的な記法非依存な構文モデルです。ファミリー付き圏の構成素は：
- 小さい圏 $`\cat{C}`$
- 反変関手 $`\mrm{T}:\cat{C}^\op \to {\bf Fam}`$
$`(\cat{C}, \mrm{T})`$ に対して拡張包括構造を公理として要求します。「複前層の圏とファミリー付き圏」で述べたように、反変関手 $`\mrm{T}`$ は次の2つの前層に分解できます。
- $`\mrm{Ty} : \cat{C}^\op \to {\bf Set}`$
- $`\mrm{Tm} : (\int_\cat{C} \mrm{Ty})^\op \to {\bf Set}`$
$`\mrm{T}`$ がファミリー付き圏の公理として要請されているので、$`\mrm{Ty}, \mrm{Tm}`$ も公理により規定されたものです。いわば、ファミリー付き圏の $`\mrm{Ty}, \mrm{Tm}`$ は“組み込み”の構成素です。
C-システムもまた、典型的な記法非依存な構文モデルです。ファミリー付き圏と同様な $`\mrm{Ty}, \mrm{Tm}`$ を定義できます。これは、後から定義できるのであって、C-システムにおける $`\mrm{Ty}, \mrm{Tm}`$ は組み込みとは言い難いです。いわば、C-システムの $`\mrm{Ty}, \mrm{Tm}`$ は“ユーザー定義”の構成素です。
対象 $`X\in |\cat{C}|`$ に対する集合 $`\mrm{Ty}(X)`$ と、$`A\in \mrm{Ty}(X)`$ に対する集合 $`\mrm{Tm}(X, A)`$ の要素は、C-システムにおいては具体的に与えられます。
- 集合 $`\mrm{Ty}(X)`$ の要素は、$`X \ILT X'`$ である2つの対象のペア $`(X, X')`$ である。
- 集合 $`\mrm{Tm}(X, A)`$ の要素は、$`\cat{C}(X, X\cdot A)`$ の要素（射）で、標準射影 $`\rho^{X, A}`$ のセクションである。
C-システムでは、「型」という概念も、「項」という概念も最初はないのです。後から定義しています。型は、2つの対象〈コンテキスト〉の架空の差分〈fictional difference〉で、項は実際のセクションです。ファミリー付き圏でも、項を、あたかもセクションのごとくに考えるのは有効ですが、実際のセクションというわけではありません。
様々な引き戻し
$`f`$ による“引き戻し”を、$`f^*(x)`$ または $`x[f]`$ と書くことが多いです。が、色々な種類の“引き戻し”が出てくるんですよね。オーバーロードし過ぎると、何がなんだかワケワカラナクなります。
$`\cat{C}`$ は構文モデルの台圏〈underlying category〉として、$`f, g`$ は次のような射だとします。
$`\quad f:X \to Y \In \cat{C}\\
\quad g:X \to Y\cdot B \In \cat{C}
`$
ナカグロ（'$`\cdot`$'）は、コンテキスト拡張の中置二項演算子記号です。
まず、標準プルバック四角形〈canonical pullback square〉の各部を次のように書くことにします。
$`\quad \xymatrix{
{X\cdot f^\diamond(B)} \ar[d]_{f^\#(\rho^{Y, B})} \ar[r]^{f \uparrow B}
\ar@{}[dr]|{\text{p.b.}}
& {Y\cdot B} \ar[d]^{\rho^{Y, B}}
\\
X \ar[r]_f
& Y
}\\
\quad \In \cat{C}
`$
- $`\rho^{Y, B}`$ は、コンテキスト拡張に伴う標準射影。
- $`f^\diamond`$ は、$`\mrm{Ty}(f)`$ の略記。
- $`f^\#`$ は、プルバック四角形によるファイバー引き戻し。ファイバー積の第一射影のこと。ファイバー引き戻しをベースの取り替え〈change of base〉とも言う。
- $`f\uparrow B`$ は、プルバック四角形によるもう一方の射影（ファイバー積の第ニ射影）。見方を変えれば、標準射影による $`f`$ のファイバー引き戻しとも言える。
もうひとつの図を描きましょう。
$`\quad \xymatrix@R+2pc@C+1pc {
{X\cdot f^\diamond(B)} \ar[d]^{\rho^{X, f^\diamond(B)} }
& {Y\cdot B} \ar[d]^{ \rho^{Y, B} }
\\
X \ar[ur]_g \ar[r]_{ f = g^*(\rho^{Y, B}) } \ar@{-->}@/^1pc/[u]^{ \mathfrak{q}^{X, Y, B}(g) }
& Y
}\\
\quad \In \cat{C}
`$
これは $`g`$ の射影分解（「拡張包括構造のもうひとつの定式化 // 拡張包括構造と射影分解」参照）の図です。
- $`g^*`$ は、プレ結合による引き戻し。$`g^*(u) = g;u = u\circ g`$
- $`\mathfrak{q}^{X, Y, B}`$ は、射影分解の第二成分を対応させるコンビネータ。
- 破線矢印は、セクションを示す。C-システムの場合は実際のセクション。ファミリー付き圏の場合は架空のセクション（$`\mrm{Tm}(X, f^\diamond(B))`$ の要素）。
- $`g^*(\rho^{Y, B}) = g ; \rho^{Y, B}`$ を $`\mathfrak{p}^{X, Y, B}(g)`$ とも書く。$`\mathfrak{p}^{X, Y, B}`$ は、射影分解の第一成分を対応させるコンビネータ。
「射影」「第一射影」「第二射影」という言葉の混乱した用法については次の記事で書いています。
項（実際の、または架空のセクション）の引き戻しを図に描くと次のようです。
$`\quad \xymatrix@R+2pc@C+1pc {
{X\cdot f^\diamond(B)} \ar[d]^{\rho^{X, f^\diamond(B)} }
& {Y\cdot B} \ar[d]_{ \rho^{Y, B} }
\\
X \ar[r]_{ f } \ar@{-->}@/^1pc/[u]^{f^{\Box B}(s) }
& Y \ar@{-->}@/_1pc/[u]_{ s }
}\\
\quad \In \cat{C}
`$
$`f^{\Box B}`$ は次のような写像です。
$`\quad f^{\Box B} : \mrm{Tm}(Y, B) \to \mrm{Tm}(X, f^\diamond(B)) \In {\bf Set}`$
$`f^\diamond`$ と $`f^{\Box B}`$ の組み合わせが、前層 $`\mrm{Tm}(\hyp, \hyp)`$ の射パートを与えます。
次の射／写像は、いずれも「引き戻し」と呼ばれます。
- $`f^\diamond`$ ： $`\mrm{Ty}(f)`$ のこと
- $`f^\#`$ ： 標準プルバック四角形によるファイバー引き戻し
- $`g^*`$ ： プレ結合による引き戻し
- $`f^{\Box B}`$ ： 項（実際の、または架空のセクション）の引き戻し
異なる種類の引き戻しが、同じ記号で書かれる（オーバーロードされる）可能性があります。
