[追記]今まで、記号／スタッフのアビタ（直接所属する圏）とアンビエント（アビタのアンダーライイング圏）を識別できてなかった気がする。[/追記][さらに追記]アビタはやめて「クラス」というありきたりの用語にした。「クラス」と「インスタンス」をペアで使う。[/さらに追記]
関手モデルとは、我々が扱う対象物を関手だとみなす考え方のこと。我々が扱う対象物を「代数系」と呼ぶとすると：
- 代数系は関手だ
となる。関手には域圏と余域圏がある。n-圏の状況で考えて、n-関手には域n-圏と余域n-圏がある。すると、代数系にも域n-圏と余域n-圏がある。代数系の域n-圏は、n-指標＝n-コンピュータッドで生成されたn-圏だとする。
- 代数系:n-圏→n圏 関手
となる。この代数系はn-関手（(n, 1)-関手）だから、n-代数系と呼ぶ。n-代数系＝(n, 1)-関手 の域n-圏はn-指標Σから生成されたn-圏なので、Σ◇ と書く。◇-閉包作用素（モナドの台関手）の定義には、メタ指標Σ'を必要とする。まーともかく、
- n-代数系:Σ◇→n圏 n-関手
となる。余域n-圏であるn-圏はメタ指標Σ'を持つメタ代数系となる。メタ指標は(n+1)-指標、メタ代数系は(n+1)-代数系となるので、
n-代数系の場合は、域n-圏がn-指標Σで一意に決まるので、プロファイルを
のように書く。
- (A:Σ --◇ A') ⇔ (A:Σ◇ → A' in n-Cat)
Σを、n-代数系Aの指標、A'を、n-代数系Aのアンビエント と呼び。(Σ --◇ A')をAのプロファイルと呼ぶ。プロファイルが(Σ --◇ A')である代数系を、A'内のΣ-n-代数系と呼ぶ。
A'内のΣ-n-代数系の全体を、nAlg(Σ, A') と書く。Σ◇の定義と、(n+1)代数A'の指標として、(n+1)指標Σ'が必要になる。これをメタ指標と呼び、nAlg(Σ, A')にメタ指標を添えて
- Σ'-nAlg(Σ, A')
と書く。Σ'-nAlg(Σ, A') の対象は、
- メタ指標がΣ'である、A'内のΣ-n-代数系
A ∈ Σ'-nAlg(Σ, A') となるので、Σ'-nAlg(Σ, A') は、代数系Aをホストしているn-圏になる。Aを直接的にホストしている圏を、Aのアビタ〈habitat | 生息域〉と呼ぶ。
アビタとアンビエントの関係は、
- アンビエントは、アビタの台n-圏〈underlying n-category〉なので、アビタからアンビエントへの忘却関手が在る。
- Aの指標Σの0-記号〈{ソート | 型}{記号 | 変数 | 名}〉のアビタはAのアンビエントである。アビタの次元は0。
- Aの指標Σのk-記号のアビタもAのアンビエントである。ただし、次元はkになる。
Σ'-nAlg(-, -):Σ'-nSig×Σ''-(n+1)Alg(Σ', A'') → Σ''-(n+1)Alg(Σ', A'') という二項n-関手があり、これは指数関手になっている。Σ'-nAlg(Σ, A') は、二項指数関手の値になっている。
- Σ'-nAlg(-, -):Σ'-nSig×Σ''-(n+1)Alg(Σ', A'') → Σ''-(n+1)Alg(Σ', A'')
- Σ ∈ Σ'-nSig
- A' ∈ Σ''-(n+1)Alg(Σ', A'')
- Σ'-nAlg(Σ, A') ∈ Σ''-(n+1)Alg(Σ', A'')
指標のタワーと代数系のタワーが、ラダーの二本の縦木だとすると、各次元ごとの二項指数関手がラダーの横木（段、踏ざん、踏み桟）になっている。縦木であるタワーは選択によって作られる。上のレイヤーで選択がなされないと、下のレイヤーにおける横木である二項指数関手を作れない。
つまり、ラダーは上から下に向かって構成する。これが、ラダーが逆帰納的であること。この逆帰納的構成は受け入れざるを得ない。
