放物線に制約された点のクラス

_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∈ ₀ C を、a~:I→C in D に対応させる。D(I, C) はDのホムシングなのでn-圏だが、ここにCをスッポリと埋め込むと C~⊆D(1, C) となる。

Cの内部構造は、D内にC~として展開されるので、Cの内部構造に言及する必要はなくなる。