曖昧性を減らす： Diag構成を事例として - 檜山正幸のキマイラ飼育記 (はてなBlog)

この記事は前半（4節まで）と後半（それ以降）に分かれています。前半では、コミュニケーションにおける曖昧性、曖昧性による行き違いを減らすための原則や手法を述べます。後半では、事例としてDiag構成について述べます。Diag構成の話題は、単なる事例というだけでなくて、内容的にも「Diag構成の再定式化・入門」となるものです。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\In}{\text{ in }}
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{\text{－} }
%\newcommand{\twoto}{\Rightarrow }
%\newcommand{\Imp}{\Rightarrow }
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\doct}[1]{\mathbb{#1}}
\newcommand{\M}{\text{-} }
\newcommand{\dimU}[2]{{#1}\!\updownarrow^{#2}}
`$

内容：

正確なコミュニケーションの方法
指標の書き方
具体例、記号の乱用、コアージョン
世界の構造
Diag構成：新しい定式化
Diag構成のためのセットアップ
別な実例
図式に関わる用語
セルって何だ？

正確なコミュニケーションの方法

前回（一昨日）の記事「デジタル語彙目録:: 動機と概要」より：

同義語・多義語の問題は、正確なコミュニケーションにとっては深刻な障害となります。
バベルの塔の神話によると、人類は神の怒りをかって、たくさんの別々な言語を話すようになったのだとか。
...[snip]...
自然言語に限らず、用語法〈テクニカルタームの体系〉においても山のような方言があり、それぞれのコミュニティが互いに「通じない違う言葉」を話しています。標準語の制定はどうせ無理なので、「通じない違う言葉」を摺り合わせて、トラブルを防ぐ算段を講じるしかないです。

「『通じない違う言葉』を話しています」は大げさな表現かも知れませんが、使うボキャブラリー（用語の集合）に対して合意が取れてない集団では、各自がてんでんばらばらな想定をしているので、実際、話が通じないんですよね。集団が二人のときでも事情は同じです。

後になって言葉の食い違いから誤解されていたことが判明すると、僕はだいぶガッカリします。ガッカリ経験はしたくはないので、正確にコミュニケートできる方法を模索しているのです。

使う用語の定義や用法〈運用ルール〉が曖昧だと、人により別な解釈をしたり、あるいは曖昧性から困惑・混乱したりします。記法に関しても曖昧性（「曖昧さを減少させるために、式にフォーマット指定 // 曖昧さ」参照）は誤解・混乱をまねきます。

この記事では、曖昧性を減らす工夫を、具体例に沿って紹介します。事例として選んだDiag構成は、だいぶ難しい概念なので、一般的な解説の事例としてはふさわしくないです。しかし、前半（最初の4節）の一般的な説明にはDiag構成の話は出てきません。前半だけ読んで事例はスキップしてもかまいません（もっとアクセスしやすい事例による説明もいずれするかも知れません）。

指標の書き方

複数の構成素〈constituent〉達から作られる構造物〈structure〉の記述には、指標〈signature〉が便利です。以下は、「デジタル語彙目録:: 動機と概要」に載せた半群の指標です。二重矢印 $`\Rightarrow`$ は集合圏の2-射ですが、等号 $`=`$ に置き換えても同じです。

$`\text{signature }\mathrm{Semigroup}\: \text{within }\mathbf{Set} \:\{\\
\quad \text{sort } U\\
\quad \text{operation } m : U \times U \to U\\
\quad \text{equation } \mathrm{assoc} ::
(m \times \mathrm{id}_{U} ) ; m \Rightarrow
\alpha_{U, U, U} ; (\mathrm{id}_{U} \times m) ; m \\
\}
`$

指標全体をLaTeX〈MathJax〉で書いているのですが、ちょっとめんどくさい。外枠はプレーンテキストで書いて、必要な数式だけをインラインLaTeXで書くことにしようと思います。少し楽ちんになります。

signature $`\mathrm{Semigroup}`$ {
sort $`U \In \mbf{Set}`$
operation $`m : U \times U \to U \In \mbf{Set}`$
equation $`\mathrm{assoc} ::`$
$`(m \times \mathrm{id}_{U} ) ; m \Rightarrow
\alpha_{U, U, U} ; (\mathrm{id}_{U} \times m) ; m \In \mbf{Set}`$
}

このブログ特有のどうでもいい話ですが、「はてなブログ」の仕様から、行頭にインデント空白を入れても表示に反映されないので、&ensp;、&emsp; でインデントしてます。

sort, operation, equation などは無くても困らないので省略します。より楽ちんになります。

signature $`\mathrm{Semigroup}`$ {
$`U \In \mbf{Set}`$
$`m : U \times U \to U \In \mbf{Set}`$
$`\mathrm{assoc} ::`$
$`(m \times \mathrm{id}_{U} ) ; m \Rightarrow
\alpha_{U, U, U} ; (\mathrm{id}_{U} \times m) ; m \In \mbf{Set}`$
}

コロンの個数で、構成素の“射としての次元”を表しています。$`U`$ はコロンがないので0-射〈対象〉ということです。コロンなしが分かりにくいなら、明示的に「対象だぞ」と書いてもいいです。

signature $`\mathrm{Semigroup}`$ {
$`U \in |\mbf{Set}|`$
$`m : U \times U \to U \In \mbf{Set}`$
$`\mathrm{assoc} ::`$
$`(m \times \mathrm{id}_{U} ) ; m \Rightarrow
\alpha_{U, U, U} ; (\mathrm{id}_{U} \times m) ; m \In \mbf{Set}`$
}

圏の対象〈0-射〉は、自明圏からの射〈ポインティング関手〉に対応するので、次のように書いてもかまいません。$`U^\sim`$ は対象に対応するポインティング関手です*1。見かけ上は、0-射に関する宣言を消去できます。

signature $`\mathrm{Semigroup}`$ {
$`U^\sim : \mbf{1} \to \mbf{Set} \In \mbf{CAT}`$
$`m : U \times U \to U \In \mbf{Set}`$
$`\mathrm{assoc} ::`$
$`(m \times \mathrm{id}_{U} ) ; m \Rightarrow
\alpha_{U, U, U} ; (\mathrm{id}_{U} \times m) ; m \In \mbf{Set}`$
}

今までの書き方はすべて、圏論をベースにした書き方です。型理論をベースにした書き方は少し違っています。

signature $`\mathrm{Semigroup}`$ {
$`U : \mbf{Set}`$
$`m : U \times U \to U`$
$`\mathrm{assoc} : \forall x, y, z:U.\, m(m(x, y), z) = m(x,m(y, z))`$
}

すべてコロンが1個なことに注目してください。型理論ベースの指標を圏論ベースの指標に書き換えることができますが、単純機械的な書き換えではなくて、若干知的判断が入ってしまいます。書き換えルールは：

矢印記号 $`\to`$ は指数型〈内部ホム型〉を表すので、混乱を避けるために $`[\hyp, \hyp]`$ に置き換える。
コロンの直後に $`\mbf{1} \to `$ を追加する。
辻褄を合わせるために、ポインティング関手を意味する $`{^\sim}`$ を付ける。コロンを一律に $`: \mbf{1} \to `$ に置き換えるための小細工です。
射の居住地〈アビタ〉を推測して追加する。型理論では居住地は暗黙化される。

このルールに従って書き換えてみると：

signature $`\mathrm{Semigroup}`$ {
$`U^\sim : \mbf{1} \to \mbf{Set} \In \mbf{CAT}`$
$`m : \mbf{1} \to [U \times U , U] \In \mbf{Set}`$
$`\mathrm{assoc} : \mbf{1} \to (\forall x, y, z:U.\, m(m(x, y), z) = m(x,m(y, z)) ) \In \mbf{Logic}`$
}

$`\text{in}`$ の後の圏（2-圏もある）は知的に推測しています。$`\mbf{1}`$ はオーバーロードされた記号で、それぞれの圏の終対象です。$`\mbf{Logic}`$ については「Propositions-As-Typesを曲解しないで理解するために」を参照してください。

指標の書き方にも方言や表記のゆれがあるわけで、「曖昧さを減少させるために、式にフォーマット指定」で述べたフォーマット指定を使うなら、次のように書き分けることになります。

we define $`\mathrm{Semigroup\M 1}`$
expression in type-theoretic-signature
$`U : \mbf{Set}`$
$`m : U \times U \to U`$
$`\mathrm{assoc} : \forall x, y, z:U.\, m(m(x, y), z) = m(x,m(y, z))`$
end.

we define $`\mathrm{Semigroup\M 2}`$
expression in categorical-signature
$`U^\sim : \mbf{1} \to \mbf{Set} \In \mbf{CAT}`$
$`m : \mbf{1} \to [U \times U , U] \In \mbf{Set}`$
$`\mathrm{assoc} : \mbf{1} \to (\forall x, y, z:U.\, m(m(x, y), z) = m(x,m(y, z)) ) \In \mbf{Logic}`$
end.

$`\mathrm{Semigroup\M 1}`$ と $`\mathrm{Semigroup\M 2}`$ は、書き方の流儀が違うだけなので概念としては区別する必要はありません。書き方の違いに過剰に反応するのはやめましょう。

具体例、記号の乱用、コアージョン

指標に出現する構成素の宣言の順番は重要です。指標で定義される構造（型理論の言葉では複合的な型）の実例を書くとき、構成素の順番を使います。例えば、次は正自然数の足し算の半群を表します。

$`\quad (\mbf{N}_{\ge 1}, \mrm{posnat\_add}, 👌)`$

一番目は半群の台集合としての正自然数の集合 $`\mbf{N}_{\ge 1}`$ 、ニ番目は半群の二項演算としての足し算です。次のような足し算関数が前もって定義されていると仮定してます。

$`\quad \mrm{posnat\_add} : \mbf{N}_{\ge 1} \times \mbf{N}_{\ge 1} \to \mbf{N}_{\ge 1} \In \mbf{Set}`$

三番目の絵文字 👌 は何なんだ？三番目は半群における結合律です。半群の実例においては、三番目のところに、“結合律が成立している証拠／証明”を提示する必要があります。が、正自然数の足し算が結合的であることは当たり前に思えます。当たり前なんですが、いざ「証明を提示しろ」と言われると困ります。なので、絵文字のOKマーク 👌 によって、「その証明は『当たり前』ってことでいいことにしようよ、大丈夫だから信用して」という意図を伝えます。

証明支援系だと、当たり前でも証明を付けないと許してくれません。証明責務のゴール（証明しなくてはいけない命題）として、次の命題〈論理式〉を突きつけられます。

$`\quad \forall x, y, z:\mbf{N}_{\ge 1}.\\
\qquad \mrm{posnat\_add}(\mrm{posnat\_add}(x, y), z) = \mrm{posnat\_add}(x,\mrm{posnat\_add}(y, z))
`$

証明しないで先に進みたいなら sorry とか書かないといけません。「当たり前のこともわからんオマエが悪いだろ、なんで俺がオマエに謝らなきゃならんのよ」と思います。

人間対人間のあいだでは 👌 で穏便に済ませましょう。

ところで、しばしば次のような記号の乱用が使われます。

$`\quad \mbf{N}_{\ge 1} = (\mbf{N}_{\ge 1}, \mrm{posnat\_add}, 👌)`$

これは、“半群”と“半群の台集合”を同じ記号で表そう、という約束です。単に「半群 $`\mbf{N}_{\ge 1}`$」と書いたら、それは足し算の半群を意味します。足し算の半群を、正自然数の集合 $`\mbf{N}_{\ge 1}`$ に対する規準的〈canonical〉な半群と言ったりします。そう言うけど、実際は規準的の真逆で、恣意的に決めた半群です。正自然数の集合を台集合とする半群として、足し算の半群を選ぶべき必然性は特にありません。「よく知ってるから」とかの心情的な理由しかないのです。

一方、記号の乱用ではなくて、半群 $`S`$ があったとします。

$`\quad S = (A, a, \text{👌})\\
\quad \text{where }a: A\times A \to A \In \mbf{Set}
`$

次のような書き方をすることは普通です。

$`\quad f:S \to \{0, 1\} \In \mbf{Set}`$

$`f`$ は集合圏の射〈関数 | 写像〉ですが、$`S`$ は集合圏の対象ではないので辻褄が合いません。この書き方の意図は：

$`\quad f:A \to \{0, 1\} \In \mbf{Set}`$

つまり、$`S`$ と書いて、$`S`$ の台集合である $`A`$ を意味したかったのです。

ひとつの記号に対して、状況に応じて（良く言えば）柔軟・融通無碍に解釈を変えていくわけです。

半群が要求されている文脈では、単なる集合を（前もって恣意的に決めた）半群だと解釈する。
集合が要求されている文脈では、半群をその台集合だと解釈する。

文脈を見ての“型変換”をコアージョン〈coercion〉と呼びます。ソフトウェアでコアージョンをするときは、コアージョン・ルールセットあるいはコアージョン・グラフというデータ構造を保持していて、それを参照してコアージョンを実行します。プログラミング言語によっては、わけわからんコアージョンをするときもあります。証明支援系では、比較的一貫したコアージョンを採用しているようです*2。

世界の構造

「最近の型理論：宇宙と世界、そして銀河」より：

語感としては、世界より宇宙のほうが広い感じがしますが、ここでは、世界は宇宙（と後述の銀河）の集まりだとします。

だんだんにサイズが大きくなるグロタンディーク宇宙の系列と、各グロタンディーク宇宙に対する集合圏、さらにはn-圏達の(n + 1)-圏達がグリッド状（下の表のよう）に配置されて世界〈world〉が形成されます。

サイズレベルが $`r`$ であるn-圏達を対象とする(n + 1)-圏は $`n\mbf{Cat}_{\# r}`$ と書きます。また、宇宙達は次のように書きます。

$`\quad \mbf{Univ}_{\# r} := |0\mbf{Cat}_{\# r}|`$

$`r, n`$ が小さい部分に関しては、フォントを変えて宇宙や銀河（銀河は $`n\mbf{Cat}_{\# r}`$ のこと）を表しましょう。以下は、「変換手意味論とブラケット記法 // n-圏」の表に宇宙を追加したものです。$`d`$ はデフォルトのレベルです。

	$`r = d `$	$`r = d + 1`$	$`r = d + 2`$
	$`\mbf{Univ}`$	$`\mbf{UNIV}`$	$`\mathbb{UNIV}`$
$`n = 0`$	$`{\bf Set}`$	$`{\bf SET}`$	$`\mathbb{SET}`$
$`n = 1`$	$`{\bf Cat}`$	$`{\bf CAT}`$	$`\mathbb{CAT}`$
$`n = 2`$	$`2{\bf Cat}`$	$`2{\bf CAT}`$	$`2\mathbb{CAT}`$

多くの作業が $`\mbf{Set}`$ 内で出来ますが、$`\mbf{Set}`$ を外から眺めるなら $`\mbf{CAT}`$ が必要になります。$`|\mbf{Set}|`$ は $`\mbf{Set}`$ の対象にはなれないので、$`\mbf{SET}`$ も必要です。という具合に、大きなサイズ／高い次元の圏が登場してきます。

圏の次元を明示的に変えたいときは $`\dimU{\hyp}{n}`$ という記法を使います。これについては「圏の次元調整」を参照してください。「変換手意味論とブラケット記法」では、自動的に（暗黙に）次元調整をしてしまうブラケット記法を導入しています。これは、コアージョンの一例です。

次元だけではなくて、サイズにおいても $`\mbf{Set} \subset \mbf{SET}`$ 、 $`\mbf{Cat} \subset\mbf{CAT}`$ のような包含がある*3ので、特に何も言わず（暗黙）に、小さなサイズのn-圏をより大きなサイズのn-圏へとコアージョンで変換（あるいは“みなし”を）します。

コアージョンに頼らずに毎回明示的に変換を書くと、非常に煩雑になるので、ある程度のコアージョンは致し方ないし、簡潔な記法をもたらします。が、暗黙のメカニズムを意識できないとマズイこともありますから、意識はしておきましょう。

Diag構成：新しい定式化

Diag構成については、次の過去記事を見てください。

この記事では、Diag構成の定義を上記過去記事とは少し変えます。

アンビエント・ドクトリンは $`\mbf{CAT}`$ に決め打ち〈固定〉する。したがって、アンビエント・ドクトリンという概念・言葉は表立っては現れない。
代わりに、ターゲット・ドクトリンという2-圏を導入する。ターゲット・ドクトリンは、$`\mbf{CAT}`$ の部分2-圏とみなせるような2-圏である。
Diag構成の一部は2-コンテナ（「2-コンテナ」参照）になる、という見方をする。
Diag構成と二項指数関手（「指数関手と構文論・意味論」参照）を容易に結び付けられるように定式化する。
グロタンディーク構成を“総和”と考えることにより、Diag構成を“多項式関手”とみなしたい。その方向で考える。

新しく導入する概念についてインフォーマルに説明しておきます。ターゲット・ドクトリン $`\doct{T}`$ とは、2-圏であって、$`\doct{T} \subseteq \mbf{CAT}`$ とみなせるものです。ほんとに部分2-圏である必要はなくて、適当な2-関手 $`U:\doct{T} \to \mbf{CAT}`$ による埋め込みがあればOKです。対象パート $`U_{\mrm{obj}} : |\doct{T}| \to |\mbf{CAT}|`$ が単射になることは要求しないので、局所埋め込み（ホム圏ごとに埋め込み）です。

「Diag構成を“多項式関手”とみなしたい」は希望／方針ですが、オリジナルの多項式関手（元祖・多項式関手）とは次のようなものです。

$`I`$ をインデキシング集合として、集合の族〈indexed family of sets〉$`C`$ を考えます。

$`\quad C : I \to |\mbf{Set}| \In \mbf{SET}`$

$`C`$ はコンテナとも呼びます。集合 $`X`$ に対して、次の集合を構成できます。

$`\quad \sum_{i\in I} X^{C(i)} \;\in |\mbf{Set}|`$

ここで、指数形式〈累乗形式〉 $`X^{C(i)}`$ の意味は：

$`\quad X^{C(i)} := [C(i), X] = \mrm{Map}(C(i), X) = \mbf{Set}(C(i), X)`$

総和記号は、無限かも知れない直和、あるいは余極限、あるいはシグマ型構成（どれも同じ意味）です。

集合 $`X`$ を動かしてやると、次のような関数が定義できます。

$`\quad P(\hyp) := \sum_{i\in I} \hyp^{C(i)} \;: |\mbf{Set}| \to |\mbf{Set}| \In \mbf{SET}`$

ハイフン〈無名ラムダ変数〉の場所には写像〈集合圏の射〉を入れることもできて、関手性〈functoriality〉も示せるので、関数から関手に昇格できます。

$`\quad P : \mbf{Set} \to \mbf{Set} \In \mbf{CAT}`$

これがコンテナ $`C`$ が定義する多項式関手です。

「Diag構成が、多項式関手の高次化／一般化を与えるといいな、与えるであろう」が僕の希望／方針であり、指導原理でもあります。とは言いながら、Diag構成の新しい定義を述べるのがこの記事の目的ではないので、本格的な記述は別な機会として、Diag構成に関わる用語・記法から曖昧性をできるだけ除去して、定義がスムーズにできるように準備します。

Diag構成のためのセットアップ

Diag構成のためのセットアップを、ひとつの構造として指標で表しましょう。ターゲット・ドクトリン $`\doct{T}`$ は、この記事で新たに導入した構成素です。

signature $`\mrm{DiagConstrSetup}`$ {
$`\cat{D} \in |\mbf{CAT}|`$
$`J:\cat{D}\to \dimU{\mbf{CAT}}{1} \In \mbb{CAT}`$
$`\doct{T} \in |\mbb{2CAT}|`$
$`U : \doct{T} \to \mbf{CAT} \In \mbb{2CAT}`$
$`\text{concrete} : \mbf{1} \to [U \text{ is } \mrm{LocallyEmbedding}] \In \mbf{Logic}`$
}

指標により定義される構造や構成素に呼び名を付けます。それを以下の形式で記述します（後に説明が続きます）。

we call $`\mrm{DiagConstrSetup}`$, Diag構成セットアップ .
for a $`\mrm{DiagConstrSetup}\: X`$
we call $`X.[\cat{D}]`$, $`X`$ の形状ドクトリン .
we call $`X.[J]`$, $`X`$ の編入関手 .
we call $`X.[\doct{T}]`$, $`X`$ のターゲット・ドクトリン .
// まだ続きあり

英文のように見えますが、英語風の人工言語です。英文としての正しさは別にどうでもいいです。指標で定義した構成素に、日本語の名前（構成素の構造における役割り名）を与えています。呼び名の取り決めは、常に恣意的なので、「なんでそう呼ぶか」に根拠はないです。根拠はなくても、決めることによりコミュニケーションに使えるようになります。

$`X.[\cat{D}]`$ は、Diag構成セットアップの実例 $`X`$ の、構成素 $`\cat{D}`$ のことです。$`\hyp.[\hyp]`$ は、構造の構成素を取り出す演算子です。よく使われる $`\hyp.\hyp`$ と $`\hyp[\hyp]`$ を、両方一緒にして、記号のコンフリクトを避けています。

圏や圏類似物が対象である圏／2-圏は「ドクトリン」と呼びます。そのほうが、用語コンフリクトや誤認・誤解を避けられると思うからです。

残りの2つの構成素は、ターゲット・ドクトリン $`\doct{T}`$ についての条件を記述しています。言いたいことは、$`\doct{T}`$ は $`\mbf{CAT}`$ への“忘却関手”を持つことです。忘却関手のひとつの定式化として、各ホム圏ごとに埋め込みになっている、という条件にしています。つまり、ホム圏 $`\doct{T}(A, B)`$ は、ホム圏 $`\mbf{CAT}(U(A), U(B))`$ の部分圏とみなせます。このことを、$`\doct{T}`$ の具象性〈concreteness〉と呼びます。

// 続き
we call $`X.[U]`$, $`X`$ の（ターゲット・ドクトリンからの）忘却関手 .
we call $`X.[\text{concrete}]`$, $`X`$ の（ターゲット・ドクトリンの）具象性 .
end.

さてここで、Diag構成セットアップの実例〈example〉を挙げます。

$`\quad (\dimU{\mbf{Cat}}{1}, \mrm{Incl}, \mbf{CAT}, \mrm{Id}_{\mbf{CAT}}, 👌)`$

Diag構成セットアップの実例には5つの構成素の具体化が必要です。上記のタプルは、5つの構成素を具体的に与えています。

形状ドクトリンは、小さい圏の2-圏 $`\mbf{Cat}`$ を1-圏とみなした $`\dimU{\mbf{Cat}}{1}`$ 。 $`\dimU{\mbf{Cat}}{1} \in |\mbf{CAT}|`$ だから、指標の宣言を満足〈satisfy〉している。
編入関手は、小さい圏を大きい圏とみなす包含関手 $`\mrm{Incl}`$ 。 $`\mrm{Incl} : \dimU{\mbf{Cat}}{1} \to \dimU{\mbf{CAT}}{1} \In \mbb{CAT}`$ だから、指標の宣言を満足している。
ターゲット・ドクトリンは、2-圏 $`\mbf{CAT}`$ 。 $`\mbf{CAT} \in |\mbb{2CAT}|`$ だから、指標の宣言を満足している。
忘却関手（2-関手）は、恒等2-関手 $`\mrm{Id}_{\mbf{CAT}}`$ 。$`\mrm{Id}_{\mbf{CAT}} : \mbf{CAT} \to \mbf{CAT}\In \mbb{2CAT}`$ だから、指標の宣言を満足している。
具象性命題（ブラケットで囲んでいる部分）の証明が必要だが、それは自明なので、OKマーク 👌 で「具象性」は成立している（証明がある）と信じてもらう。

実例は、構成素の順番により記述してかまいませんが、指標で使われていた構成素役割り名との対応を取りたいなら、次のように書くとハッキリします。

$`\quad (\cat{D} := \dimU{\mbf{Cat}}{1}, J := \mbf{Incl}, \doct{T} := \mbf{CAT}, U:= \mrm{Id}_{\mbf{CAT}}, \text{concrete} := 👌)`$

別な実例

Diag構成セットアップの別な実例を見てみましょう。

$`\quad (\mbf{FinSet}, \mrm{DiscCat}, \mbf{CartCAT}, \mrm{ForgetCart}, 👌)`$

5つの構成素の具体化は：

形状ドクトリンは、有限集合の圏 $`\mbf{FinSet}`$ 。 $`\mbf{FinSet}\in |\mbf{CAT}|`$ だから、指標の宣言を満足している。
編入関手は、集合を離散圏〈discrete category〉とみなす関手 $`\mrm{DiscCat}`$ 。 $`\mrm{DiscCat} : \mbf{FinSet} \to \dimU{\mbf{CAT}}{1} \In \mbb{CAT}`$ だから、指標の宣言を満足している。
ターゲット・ドクトリンは、デカルト圏〈Cartesian category〉達の2-圏 $`\mbf{CartCAT}`$ 。 $`\mbf{CartCat} \in |\mbb{2CAT}|`$ だから、指標の宣言を満足している。
忘却関手（2-関手）は、デカルト圏のデカルト構造を忘れる2-関手 $`\mrm{ForgetCart}`$ 。$`\mrm{ForgetCart} : \mbf{CartCAT} \to \mbf{CAT}\In \mbb{2CAT}`$ だから、指標の宣言を満足している。
具象性命題は、デカルト構造を忘れることが、関手と自然変換のレベルでは同一性を保つこと。その証明は自明ではないが、👌 で「具象性」は成立している（証明がある）と信じてもらう。信じない人もいるだろうが。

もうひとつの例は次です。

$`\quad (\mbf{Graph}, \mrm{FreeCat}, \mbf{CAT}, \mrm{Id}_{\mbf{CAT}}, 👌)`$

形状ドクトリンは、グラフ〈有向グラフ〉の圏 $`\mbf{Graph}`$ 。 $`\mbf{Graph}\in |\mbf{CAT}|`$ だから、指標の宣言を満足している。
編入関手は、グラフから自由圏〈パスの圏〉〈free category〉を作る関手 $`\mrm{FreeCat}`$ 。 $`\mrm{FreeCat} : \mbf{Graph} \to \dimU{\mbf{CAT}}{1} \In \mbb{CAT}`$ だから、指標の宣言を満足している。
ターゲット・ドクトリンは、圏達の2-圏 $`\mbf{CAT}`$ 。 $`\mbf{Cat} \in |\mbb{2CAT}|`$ だから、指標の宣言を満足している。
忘却関手（2-関手）は、恒等2-関手 $`\mrm{Id}_{\mbf{CAT}}`$ 。$`\mrm{Id}_{\mbf{CAT}} : \mbf{CAT} \to \mbf{CAT}\In \mbb{2CAT}`$ だから、指標の宣言を満足している。
具象性命題（ブラケットで囲んでいる部分）の証明が必要だが、それは自明なので、OKマーク 👌 で「具象性」は成立している（証明がある）と信じてもらう。

前節の実例も入れると3つの実例を出しました。編入関手は次のようでした。

$`\mrm{Incl} : \dimU{\mbf{Cat}}{1} \to \dimU{\mbf{CAT}}{1} \In \mbb{CAT}`$
$`\mrm{DiscCat} : \mbf{FinSet} \to \dimU{\mbf{CAT}}{1} \In \mbb{CAT}`$
$`\mrm{FreeCat} : \mbf{Graph} \to \dimU{\mbf{CAT}}{1} \In \mbb{CAT}`$

これがコンテナに対応します。コンテナ〈ファミリー〉と編入関手の類似性は、次の形に書いてみるとハッキリするでしょう。

$`C : I \to \dimU{(0\mbf{Cat}_{\# 1})}{0} \In 0\mbf{Cat}_{\# 2}`$ （コンテナの例）
$`\mrm{FreeCat} : \mbf{Graph} \to \dimU{(1\mbf{Cat}_{\#2})}{1} \In 1\mbf{Cat}_{\# 3}`$ （編入関手の例）

Diag構成セットアップでは、次元もサイズも1つ上がっています。

図式に関わる用語

この節では、Diag構成に関するコミュニケーションを難しくしている曖昧性を減らす約束事を決めていくことにします。

Diag構成の"diag"は図式〈diagram〉のことです。「図式」という言葉は曖昧多義語ですが、Diag構成の文脈では関手のことです。関手は、関手圏の対象です。なので、次のように呼び名の定義ができます。

for $`A \in |\cat{D}|`$ and $`\cat{T}\in |\doct{T}|`$
we call an object of $`\mbf{CAT}(J(A), U(\cat{T}))`$, 図式 .
end.

2-圏 $`\mbf{CAT}`$ 内で考えれば、図式は次のような1-射〈関手〉です。

$`\quad D : J(A) \to U(\cat{T}) \In \mbf{CAT}`$

図式 $`D`$ の「ソース」と「ターゲット」を定義したいのですが、候補が複数あります。

$`A\in |\cat{D}|`$ が $`D`$ のソース
$`J(A) \in |\mbf{CAT}|`$ が $`D`$ のソース
$`\cat{T}\in |\doct{T}|`$ が $`D`$ のターゲット
$`U(\cat{T})\in |\mbf{CAT}|`$ が $`D`$ のターゲット

ウーム、「ソース」「ターゲット」は使うのやめて、次のようにしようかな。

for $`D : J(A) \to U(\cat{T}) \In \mbf{CAT}`$
we call $`A`$, $`D`$ の形状 .
we call $`J(A)`$, $`D`$ の域圏 .
we call $`\cat{T}`$, $`D`$ のキャンバス .
we call $`U(\cat{T})`$, $`D`$ の余域圏 .
end.

「図式」がお絵描きのイメージなので、同じフレーバーの「形状」「キャンバス」で揃えようと。定義としては、$`D`$ は関手ですが、気持ち〈メンタルモデル〉としては、決められた形状（概観）を自分の裁量でキャンバスに描画する行為が $`D`$ だ、と。気持ちのなかでは、以下のような仮想的な射（波線）があるわけです。

$`\quad \xymatrix{
A \ar@{~>}[r] \ar@{|->}[d]_{J}
& \cat{T} \ar@{|->}[d]^{U}
\\
J(A) \ar[r]^{D}
& U(\cat{T})
}`$

「形状」は、関手としての図式の域圏ではなくて、域圏のもとになる対象と約束しましたが、「形状」を別な意味でも使うことにします。

for a $`\mrm{DiagConstrSetup}`$ $`X`$
we call an object of $`X.[\cat{D}]`$, 形状 .
end.

形状ドクトリンの対象も「形状」と呼ぶことにします。「形状」は曖昧多義語になります。が、用法が違うので、それほど混乱することはないでしょう。「図式の形状」は、図式あっての用語です。このことをハッキリさせたいなら、図式を構造として定義して、「形状」は構成素役割り名とします。次のようです。

signature $`\mrm{Diagram}`$ {
$`A\in |\cat{D}|`$
$`\cat{T} \in |\doct{T}|`$
$`F : J(A)\to U(\cat{T}) \In \mbf{CAT}`$
}

for a $`\mrm{Diagram}`$ $`D`$
we call $`D.[A]`$, $`D`$ の形状 .
we call $`D.[\cat{T}]`$, $`D`$ のキャンバス .
we call $`D.[F]`$, $`D`$ の関手 .
we call $`\mrm{dom}(D.[F])`$, $`D`$ の域圏 .
we call $`\mrm{cod}(D.[F])`$, $`D`$ の余域圏 .
end.

さらに、記号の乱用の約束もしておきましょう。

$`\quad D = D.[F]`$ （乱用、ほんとの等号ではない）

構造としての図式と、その「関手」という構成素を区別しないことになります。

セルって何だ？

図式の余域圏が集合圏の場合を考えます。この場合、図式とは次の関手圏の対象です。

$`\quad \mbf{CAT}(J(A), \mbf{Set}) \; \in |\mbf{CAT}|`$

$`D:J(A) \to \mbf{Set}`$ を図式とします。$`J(A)`$ は圏ですから、そのなかに射があります。

$`\quad f:a \to b \In J(A)`$

$`D`$ による値は集合圏のなかに居ます。

$`\quad D(f):D(a) \to D(b) \In \mbf{Set}`$

図式 $`D`$ の「セル」は何を意味するでしょうか？圏 $`J(A)`$ の対象でしょうか？それとも、集合 $`D(a)`$ や $`D(b)`$ の要素でしょうか？ $`J(A)`$ の射は「セル」と呼んではマズイでしょうか？また、セルの次元とは何でしょうか？

これらの疑問に答えるには、今までのDiag構成セットアップだけでは不十分です。形状（形状ドクトリンの対象）や編入関手に追加の構造・性質が必要になります。（この記事内では明確化の作業はしませんが。）

実情としては、形状 $`A`$ の居住者〈inhabitant〉を「セル」と呼ぶこともあれば、域圏 $`J(A)`$ の居住者を「セル」と呼ぶこともあるし、関手の像である集合圏の居住者*4を「セル」と呼ぶこともあります。何の交通整理もしないままでは、「セル」という言葉は危なくて使えません。

「セル」以外にも人により解釈や連想が変わってしまう言葉はあります。だから、摺り合わせと合意の手段が必要なのです。

*1:$`U`$ と $`U^\sim`$ を同一視してもかまいません。その場合は、議論の舞台が $`\mbf{Set}`$ から $`\mbf{CAT}`$ に持ち上がります。

*2:型システムのなかに、まっとうなコアージョンを組み入れることも出来ます。

*3:ラッセル方式の宇宙系列を考えた場合です。「最近の型理論：宇宙・世界・銀河もう少し」、「型・インスタンス・宇宙とタルスキ宇宙系列」参照。

*4:要素とポインティング写像を同一視すれば、要素も次元1の居住者です。