指標の構造

高次圏論 セオリー論

色々とゴタゴタだが、重要な概念。

1-指標の種

まず、知り方＝「『知っている』のあり方」として、

  • 直接知〈direct knowledge〉＝直接知っていること、経験的に知っていること
  • 公理的知〈axiomatic knowledge〉＝公理系の実例として知っていること

とに分類する。

1-指標に関して、その種〈kind〉（複数かも知れない）とは、アンビアント圏（複数かも知れない）の種類（2-指標で定義される）を指定する記号のこと。具体的アンビアント圏の知り方として、

  • 具体的アンビアント圏を直接知っている（例：Setを経験的に知っている）
  • 具体的アンビアント圏を公理的に知っている（例：Setをデカルト・モノイド閉圏の実例として知っている）

具体的アンビアント圏を直接知っているときは、「knowing 1-category 具体的アンビアント圏」という形で具体的アンビアント圏を指定する。

アンビアント圏を公理的に知っているときは、「using 2-signature 親指標」という形でアンビアント圏の種〈2-型〉を指定する。親指標の特定モデル〈インスタンス〉の指定が、1-指標の種の具体化になる。

「種」と「アンビアント圏」はほぼ同義語（記号と意味の関係）。具体的種は具体的アンビアント圏（を表す記号）のことで、一般的種は一般的アンビアント圏のこと。一般的アンビアント圏（の記号）は具体的ではないから、2-指標によって定義される。

1-指標に対して、その種は、型変数〈0-変数〉の変域、関数変数〈1-変数〉の変域、等式変数〈2-変数〉の変域を与える。モデル＝インスタンス＝具体化は、各種変数に具体化的アンビアント圏の具体的射を割り当てること。割り当てに際して、プロファイル条件（射の両端制約、境界条件）を守る必要がある。

1-指標には、その具体的または一般的アンビアントを指定する必要があるので、次のどちらかを指定する必要がある。

  1. 種をソート〈型 | 1-変数〉として定義している親指標（2-指標）を指定する。
  2. 具体的種を指定する。

それが前述した：

  1. using 2-signature 親指標 （種名は、親指標の型名）
  2. knowing 1-category 圏 （種名は、圏名）

usingを使い続けると、親指標のタワー（というよりツリー）は無限に成長する。無限ツリーを認めるか、knowingで止めるかのどちらか。

1-指標と次元

1-指標の1は指標の次元だが：

  • 1-指標： アンビアントは1-圏である。例： マグマ、モノイド、ベクトル空間、モノイド作用集合
  • 2-指標： アンビアントは2-圏である。例： モノイド圏、デカルト閉圏、モナド、随伴系、ベックの分配法則

n-指標の次元は、アンビアントの圏次元と一致するので、n-指標の記号の次元は、0, 1, ..., n, n + 1 となる。n + 1 は常に等式だとする。

指標の種とは、具体的アンビアントか、または一般的アンビアントの種別なので、

  • 具体的n-圏を指定する。
  • 構造付きn-圏を定義する (n+1)-指標を指定する。

のどちらかをする。

n-指標をコンピュータッドとみて生成される自由圏はn-圏。自由n-圏からアンビアントであるn-圏への関手（(n, 1)-関手）が指標のモデル〈インスタンス〉になる。モデルを対象とする圏は再びn-圏になるので、モデルの圏もn-圏である。例えば、2-指標の、2-圏をアンビアントとするモデルは2-圏となる。モデル2-圏の対象、1-射、2-射は、関手〈(2,1)-関手〉、自然変換〈(2,2)-関手〉、変更（(2,3)-関手）になる。

指標が要求する記号と提供する記号

指標は記号の集まりを提供する〈定義する | エクスポートする | 導入する〉。そして、記号を要求する〈使用する | 消費する〉。

signature Monoid {
 0-mor A
 1-mor m:A×A→A
 1-mor e:I→A
 2-mor assoc:: (m×id[A]);m ⇒ (id[A]×m);m
 2-mor lunit:: (e×id[A]);m ⇒ id[A]
 2-mor runit:: (id[A]×e);m ⇒ id[A]
}

この指標は、外の種（構造付き圏）が厳密デカルトモノイド圏と仮定している。

  • 提供する記号： A, m, e, assoc, lunit, runit
  • 供給する記号： ×, I
  • 事前に了解されている定記号： (;), id[-]

部分指標と忘却関手

モノイド指標の部分指標として、

  1. 付点集合の指標
  2. 半群の指標
  3. 集合の指標
  4. マグマの指標

などがある。これらの部分指標の埋め込みと、忘却関手が対応する。忘却関手は、指標で定義された構造的型の圏から、アンビアント圏（の直積）への関手になる。

指標の構文的分類

次の分類軸を設ける。

  1. 次元 {0, 1, 2, ...}
  2. ソート数 {単ソート, 多ソート}
  3. ソート種 {同種, 異種}

異種単ソートはないが、その他は直交した分類軸。

ソート（型）の種がアンビアント。同種〈ホモジニアス〉の指標のアンビアントは、ひとつの圏の直積。異種〈ヘテロジニアス〉指標のアンビアントは複数の圏の直積。