指標と仕様と等式的と述語的
指標とコンピュータッドはまったく同義語だとする。指標の理論とはコンピュータッドの理論。
- (具体)指標=コンピュータッド=ポリグラフ=(高次)箙
コンピュータッドは、背景としている形状により定義が変わるが、ここでは常に球体形状〈globular shape〉。
仕様と指標の本質的な違いはない。仕様は指標の一種であり、高次元部分を表明〈assertion〉と呼ぶと、それは仕様になる。何を表明と呼ぶかの基準はないので、仕様と指標の区別も基準はない。
最も重要な仕様は、n-圏の(n + 1)-指標である。n-圏の(n + 1)-射は等式しかないので、必然的に、指標の(n + 1)部分〈(n + 1)-part | (n + 1)-section〉は、n-射の等式の集まりになる。この形の指標を等式仕様(等式的仕様)と呼ぶ。等式は無限個あってもよい。
述語とは、特定の基準対象〈criterion object〉への射である。0-基準対象はブール集合、1-基準対象は集合圏である。各次元の基準対象は持ち上げ〈lift〉と落とし込み〈drop〉ができる。
真射〈truth morphis〉とは、任意の対象から基準対象への射で、自然変換として決っている。τX:X→B 。トポスではサブオブジェクト・クラシファイアだが、一般的な特徴付け=公理化はよく分からない。
真射以外に、X上のブール値定数関数に相当する命題射(または真偽値)が定義できる。X上の命題射は、基礎対象からの命題射=真偽値を、基礎対象=終対象への唯一射〈bang〉で引き戻したもの。
述語射と命題射の組を表明のフォーマットに採用した仕様を述語仕様(述語的仕様)と呼ぶ。
n-圏に対する述語仕様は、形式上はn-指標である。n-射までしか登場しないから。しかし、実際は等式仕様になる。述語と真偽値の組を、等式とみなして、(n + 1)-セルとして追加すれば、対応する等式仕様ができる。
- 述語仕様は、等式仕様の略記である。
コンピュータッドと圏の関係を考える上で、等式仕様は重要である。圏Cに対して、どのような指標を作るかは自明ではない。特に高次圏では難しい。
n = 1のケースでは、1-圏Cに、2-指標(1-等式仕様)Σを対応させる。
- Σ0 = |C|0 = Obj(C)
- Σ1 = |C|1 = Mor(C)
- Σ2 = (別記)
Σ2 は次のようにする。1-指標 (Σ0, Σ1)の上にグラフの圏を作る。グラフの辺は、[A, f1, ... , B] の形。次の等式をすべてΣ2に入れる。
- [A, f, g, C] = [A, f;g, B]
- [A, idA, A] = [A, A]
2-指標Σから生成される1-圏は、Σ0, Σ1から生成されるグラフに、Σ2の等式達から生成される最小の同値関係による商となる。
こうして作った圏をΣ◇とする。圏から等式仕様を作る操作を C! とすると、C!◇ C が成立する。