なんというバカバカしさ、なんという無駄、なんという浪費！
| ラムダ計算 | インスティチューション | 型理論 |
|---|---|---|
| 型コンテキスト | 指標 | 型前提（域側） |
| 大きなラムダ式 | クライスリ指標射 | 型判断（シーケント） |
| 大きなラムダ計算 | 指標圏の計算 | 型証明計算 |
| レコード（値環境） | 点指標射（指標圏の点射） | 型証拠（ハビテーション） |
| レコードの圏 | ソフトモデル圏（指標コスライス） | - |
プログラミング：
| インスティチューション | 関数型 | オブジェクト指向 | データベース |
|---|---|---|---|
| 指標 | 型クラス, 指標 | インターフェイス | テーブルスキーマ |
| クライスリ指標射 | ファンクタ | アダプターパターン | データマイグレーション |
| 指標圏の計算 | - | - | - |
| 点指標射（指標圏の点射） | ストラクチャ, レコード | クラスインスタンス | テーブル行 |
| ソフトモデル圏 | ストラクチャとファンクタ | アダプタープログラミング | - |
集約・統合・圧縮のとき、けっこう邪魔になるのが、要素と点の違い。
- 要素： 集合論的な実体（モノ）
- 点 ＝ 点射 ： 終対象または単位対象からの射
それと、指数型の対象とホムセットの混同、つまり、指数対象への点射と、反カリー化した射の区別が出来ない。
