指標と仕様と表明
nに対して、n-指標はn-セル＝n-項までを持つコンピュータッドとして定義される。n-指標はn-コンピュータッドだから、n-圏を生成する。このn-圏に、(n+1)-射の族を追加する役割が(n+1)-表明。n-指標と(n+1)-表明の組み合わせがn-仕様（(n+1)-仕様ではない）。
- n-仕様 ≒ (n+1)-指標
だがイコールではない。微妙な差がよく分かってない。
とりあえず表明〈assertion〉の構文だが、
- ∀{ ここにn-指標 } ⇒ (n+1)セルの定義
型シーケント＝型文脈と似ている。だが、⇒の左に出てくる指標の名前は束縛変数であり、特定の射を表してない。左辺はパターンなのだ。「左辺のパターンが出現したとき、右辺のセル（射）を生成していい」が表明の意味。
等式的表明の場合は、
- ∀{ ここにn-指標 } ⇒ α = β
αとβはn-式で、左辺の束縛変数と、指標部分で出現した名前（項目）を使って組み立ててよい。等号が(n+1)-射を意味していて、等号だから恒等射であるという制約がある。また、意味である圏がn-圏だとすると、(n + 1)以上は潰れているから、等式に対応する射は存在しても1個である。
ソフトウェア的に考えると、指標部分には宣言と定義しかない。これはオペレーター＝オペレーションコマンドで実装する。オペレーションコマンドは、実は何もしなくて、式を生成するだけ。その式を評価／還元することはない。
一方、表明、特に等式的表明はリライターで実装される。リライターはオペレーターとしても使える。オペレーター機能（式の生成機能）にさらに、式の評価／還元機能を持っている。生成と評価／還元をワンタイミングでやることをリライトと呼ぶ。
オペレーターとリライターを作ってみて、動かしてみると謎が解けるかもしれない。おそらくは、階層的・段階的なリライトという概念があるのだと思う。= と ⇔ が似ているのは、それが最上位にあるときはリライターとなるからだろう。
- 算数では、+や*はリライターである。= の判定は自明。
- 記号算では、+や*はオペレーターで、=はリライターとなる。それとは別に、等式のあいだの⇔の判断があり、自明ではなく、等式的論理レベルのリライターがある。
- 論理計算では、⇔はオペレーターで、命題の書き換えのリライターがある。
次のようなリライターが登場した。
- 具体的な数の計算のリライター
- 代数式（文字式）のリライター
- 等式のリライター
- 論理式のリライター
これらの階層性・段階性を考える。
