_R のような下線で始まる語は太字の代替で、固有名詞(特定インスタンスを指す名前)となる。
次元ごとに付けるキーワードは恣意的なので括弧に入れることにした。
1-sinature movable { 0(sort) S in _Set 1(mathod) moveBy:S×_R→S in _Set 2(equation) assco:: for s in S. moveBy(moveBy(s, x), y) = moveBy(s, x+y) : S×_R×_R→S in _Set 2(equation) unit:: for s in S. moveBy(s, 0) = s : S→S in _Set }
0-signature parabola { 0(slot) x in _R 0(slot) y in _R 1(constraint) con: x*x = y in _R }
この2つの指標を組み合わせると、「放物線内に成約された点」のクラスが出来ると思うが、その構造を分析せよ。
一般に内部〈content〉を持つ台対象があり、内部の仕様も指標で書いたものがクラス定義になる。クラス定義を指標の立場から言えば、次元が異なる指標の組み合わせ。0次元指標のクラス(レコード集合)が、1次元指標の台対象(アンビエント圏の対象)を与える状況。
ここでも、対象とそのアロー化リフトである点射〈point morphism〉の関係を使っているような気がする。
アロー化リフトの解説:
n-圏Cを(n+1)圏D内で扱う方法のひとつ。n-圏Cは、内部に0-射からn-射を持つが、それを、外の(n+1)-圏Dの1-射から(n+1)-射に対応させて持ち上げる。キュリアの格上げと呼んでいたテクニック。
アロー化するには、外の(n+1)-圏Dに単位対象が必要。単位対象をIとして、a∈ 0 C を、a~:I→C in D に対応させる。D(I, C) はDのホムシングなのでn-圏だが、ここにCをスッポリと埋め込むと C~⊆D(1, C) となる。
Cの内部構造は、D内にC~として展開されるので、Cの内部構造に言及する必要はなくなる。