ハイパーインスティチューション

	ハイパードクトリン	インスティチューション
ベース対象	型コンテキスト	指標
ベース射	コンテキスト拡張／置換	指標射
ファイバー	命題の圏	モデルの圏
誘導関手	引き戻し	リダクト関手
随伴関手	限量子	-
妥当性	-	充足関係

こうして見ると、限量子随伴性がハイパードクトリンの特徴で、充足関係がインスティチューションの特徴ということになる。

ハイパーインスティチューションを定義するには、

1. 限量子随伴をインスティチューションに取り込む。
2. 充足関係をハイパードクトリンに取り込む。

我々の目的は型クラスのセマンティクスなので、ハイパーインスティチューションのグロタンディーク平坦化がうまくできないと困る。

1. 型クラス（＝対象）のインスタンシェーションがうまく定義できる。
2. 型クラス（＝対象）のコンビネータがうまく定義できる。
3. トランスレーション（＝射）がうまく定義できる。
4. トランスレーションのコンビネータもうまく定義できる。

それで、次ができないと困る。

• マグマ、モノイド、群などの階層構造が定義できる。
• モノイドと可換モノイドを"継承して”半環型クラスが定義できる。
• 代数的ベキ等可換モノイドと順序的半束が型クラスとして同値であることを証明できる。

ということは、型クラスの圏の上にもう一度なんらかの論理が定義出来ないといけない。型クラスを型として、型クラスのすべてのインスタンス上を走る変数を導入した一階述語論理だろう。

• ∀M:IdempMonoid.∃L:SemiLattice, F:L->M, G:M->L.( F*G = Id_SemiLattice ∧ G*F = Id_IdempMonoid )