ハイパーインスティチューションの構成法
素材：
以上から、指標圏と指標射が作れて、指標圏を定義できる。この指標圏をベース圏として、論理ドクトリンLに値をとるインデックス付き圏をプレ・ハイパードクトリンと呼ぶ。プレ・ハイパードクトリンであって、ΣΔΠ随伴性を持つものを、Name, C上のハイパードクトリンと呼ぶ。ハイパードクトリンは、だいたい述語論理の構文論に対応する。ただし、アンビエント圏Cは基本的なセマンティクスに関係する。例えば、ハイパードクトリンにおける型はCの対象を意味する。
ハイパードクトリンは指標圏の上のインデックス付き圏なので、グロタンディーク平坦化を実行できる。ハイパードクトリンのグロタンディーク平坦化圏をグロタンディーク／エルブラン圏と呼ぶ。
グロタンディーク／エルブラン圏は、有限余完備圏になるので、貼り合わせ構成が出来る。この貼り合わせが大局的プログラミングに相当する。もとのアンビエント圏、またはベース圏（アンビエント圏と名前から作った圏）における射（＝プログラム）の構成が小局プログラミング。
グロタンディーク／エルブラン圏に対して余スライス構成をして作ったインスティチューションをハイパーインスティチューションと呼ぶ。Modの作り方は自明だが、Senがいまいち分からない。
- ハイパーインスティチューション＝ハイパードクトリンのグロタンディーク／エルブラン圏上の余スライス・インデキシング。
