うーん、ラムダ計算かぁ？
最初に与えられるハイパードクトリンとエルブランモデルで作られるインスティチューションをレイヤー0（L0）と言うことにする。L0の上にレイヤー1インスティチューションを構成するのが問題なのだが、結局、レイヤー1はレイヤー0と同型である、という事だと思う。ただし、レイヤー1はレイヤー0よりはるかに使いやすいので、人はレイヤー1を使う。
- 上昇埋め込み定理： レイヤー0はレイヤー1にインスティチューションとして埋め込める。
- 下降レイフィケーション定理： レイヤー1はレイヤー0にインスティチューションとして埋め込める。
レイヤー1のベース射はtransformerと呼ぶことにしする。ディヴィジョンのラベリングはとりあえず次のようにする。
| レイヤー | ベース対象 | ベース射 | 基礎射 | ファイバー対象 | ファイバー射 |
|---|---|---|---|---|---|
| レイヤー0 | type | function | value | predicate | implication? |
| レイヤー1 | signature | transfromer | structure | proposition | theorem |
レイヤー1に関しては、ベース圏の反対圏が非常に重要になる。ベース圏の反対圏の射をoptransformerとopstructureと呼ぶ。ただし、矢印の向きを反対にする以外の差はない。インスティチューションの定義のときは、反対圏を使うことになる（そうでないとインデックス付き圏の定義に反する）。
ML用語（@ML）との比較は：
- signature@ML は signature
- structure@ML は structure
- functor@ML は transformer
実は、レイヤー1のベース圏はデカルト閉圏になる。この事実に気が付きにくいのは次の理由：
- 指標に直和が定義できる。が、非モノイド直和である。リネーマ（リネーミングtransfomer）を使わないと直和が構成できない。up-to-renameな議論。
- 始対象は空指標だが、これは一意に定義できる。
- 非モノイド・デカルト圏になるのは、transformerの圏ではなくて、optransformerの圏。
- つまり、直和を非モノイド直積としたデカルト圏上の閉構造となる。
カリー同型を書くと：
OpTran(Σ#Δ, Γ) ------------------- 同型 OpTran(Σ, Δ-^Γ)
フルカリー化だと：
OpTran(Σ, Γ)
------------------- 同型
OpTran({}, Σ-^Γ)型付きラムダ抽象を λΔ.t と書く。通常のラムダ計算と同じ記法。LambdaΔ{t} でもいいかも知れない。Δはブレイスかパーレンで囲むんで、直前のLambdaとΔは並べても大丈夫。tもブレイス囲みだから、追加の囲み{}も不要かな。
適用演算子は◁とする。通常は、◁が明示されずに、
- (λΔt)◁A を t[A] と書く。
- ここで、Aはtransformer項だが、structureしか使わない。
問題点がいくつかあって、
- 基礎射であるstructureと外部モデルであるstructureが区別されてない。
- morophism（射）とopmorphism（反射）の区別がされてない。
- 適用演算子と結合演算子が導入されてない。
- 非モノイド的直和演算子さえ導入されてない。
解決のための考慮点：
- 非モノイド直和演算子を導入する。
- リネーマとリネーマの適用の構文を決める。特別な構文を設けずに変換子として扱うことも考えられる。
- 変換子の結合と適用の演算子を導入する。
- 変換子の余田プリングの演算子を導入する。
候補
- 直和演算子 #
- 非対称直和演算子 #<, ># （オーバーライド :!, :=! などが使える）
- 始対象 {}, Θ
- 結合 <<, >>, ▶, ◀
- 適用 <, >, ◁, ▷
- パラメータ化 param Δ, πΔ.
- ラムダ抽象 lambda Δ, λΔ.
- 余タプリング [, ]
- リテラル {}
- 反対化 ()~
- 大きなラムダ式 (Δ | t)、プロファイル付き (Δ | t : Σ)。
変換子のプロファイルは、要求指標（ソース）と保証指標（ターゲット）で決まる。変換子の項だけでは決まらない。変換子項のリテラルは、ミックスリテラルで書かれる。
- 純指標リテラル： ディヴィジョニングとプロファイリングの集まり
- 純変換子リテラル： アタッチングの集まり
- ミックスリテラル： ディヴィジョン、プロファイリング、アタッチングの集まり。ひとつでもアタッチングが入れば、それは指標（インターフェイス）ではなくて変換子（実装クラス）と考える。
オブジェクト指向との関連：
| レイヤー1 | オブジェクト指向 |
|---|---|
| 純指標 | インターフェイス |
| 純変換子 | 実装クラス |
| 混合 | 抽象クラス |
指標と変換子の両方を表現できる構文形式としてレコードを考えるといいかも知れない。
- 指標レコード : ディヴィジョニングとプロファイリングだけのレコード
- 変換子レコード : アタッチングだけのレコード
- 混合レコード： 指標レコードでも変換レコードでもない。
指標レコードと、適当な（混合でもいい）レコードの組 (Δ| t) が扱うべきもの（ある種のシーケント）で、項tだけのときは、tの自由指標を取り出してΔとして、(Δ | t) を作る。基本操作は、
- tのターゲット指標＝保証指標を求める。
- 混合レコードを分離して、恒等変換子と非恒等変換子に分ける。
ともかくも、レイヤー1のベース圏は、非モノイド的余デカルト閉圏であり、余ファイバー余和＝融合和も持ち、有限余完備であることがわかった。余デカルト閉圏の指数は余指数と呼べばいいかな。
