変数の圏
変数、つまり、後から意味を割り当てられる名前のことだが、その集合達は圏をなす。どういう圏であるかを調べておく。
まず、たかだか可算の集合を対象として、単射を射とする圏をωInjとする。変数の圏はωInj上の具象圏でなくてはならない。一般的にVが変数の圏だとは：
- 始対象を持つ。（具象性から、始対象は空集合）
- コファイバー和（融合和、貼り合わせ）を持つ。
- ファイバー積を持つ。
ファイバー積は、埋め込みの共通部分で与えられる。始対象とコファイバー和から、直和を持つ。しかし、終対象を持つとは限らないので直積は保証されない（使わない）。
一般に、A∈Cが概終対象（almost final object）だとは：
- 任意のXからAへの射が存在する。
- f, g:X→A があるとき、fとgはAut(A)の違いしかない。
つまり、AのAut群を法として、X→Aは一意的と言える。変数の圏に概終対象の存在を要求することもあるが、必須ではない。むしろ、ある種の有向性のほうが大事：
- A, Bに対して、A→C, A→C が存在し、ファイバー積A∧Bが0になるCがある。
指標Σに対して、アンビエント・モデル圏Aへの意味関手（の生成系）F:Σ→Aがあるとき、S=Sort(Σ)としてのS-ソート付き変数集合Xに対して、[X]F∈|A| が決まる。[-]Fは、変数圏VからAへの関手となる。
VとΣを一緒にして扱うにはウエス計算。Vの対象XごとにXとソート列を繋ぐ形式的な同型を1個ずつ作って、ΣにVをアタッチする。Σ∪fV（fはアタッチメント）を作って、もう一度自由圏を作る。→リカバる -- 考え直す - 檜山正幸のキマイラ飼育記 メモ編
具体的にVを作るには、名前の不変集合Uを準備して、Pow(U×N) のなかで、高さ有限で単葉（Uへの射影が埋め込み）な集合を使うのがいいだろう。
