インスティチューションは重要だと思っているのですが、このブログでまとまった記述をしたことはありません。じゃ、まとまったものを書くのか -- 書きません(苦笑)。まとまりのない断片的なことを書きます。
インスティチューションはインデックス付き圏です。ベースの圏（インデックスの圏）は指標圏（category of signatures）と呼ばれ、標準的な記法では Sig と書きます。指標 Σ∈|Sig| ごとにモデル圏 Mod[Σ] が対応して、Σ |→ Mod[Σ] がインデックス付き圏の構造を与えます。ρ:Σ→Γ in Sig に対する Mod[ρ]:Mod[Γ]→Mod[Σ] をリダクト関手（reduct functor）と呼び、通常は ρ* と書きます。
インスティチューションは、この他に、論理文（logical sentence）の集合と充足関係（satisfaction relation）を持ちますが、今回の話には関係ありません。（よって、これ以上触れません。）
さて、「型とはなんでしょう？」 -- この問に正解はありません。いくつかの立場があるだけです。その立場を、*-as-Types とか Types-as-* とか呼ぶことがあります。
- Sets-as-Types
- Algebras-as-Types
- Coalgebras-as-Types
- Propositions-as-Types
インスティチューションの枠内で考えるとして、型はインスティチューションのどこに現われるのでしょう？ 2つの候補があります。
- 指標（指標圏の対象）が型である。
- モデル（モデル圏の対象）が型である。
1番目の立場を採用すると、指標Σにはモデル圏Mod[Σ]が付随するので、「モデル圏が型である」と言ってもいいでしょう。つまり、Categories-as-Types となります。
しかし、モデル圏全体ではなくて「モデル圏の対象が型である」と考えるほうが多数派でしょう。幸いに、多くの実用的ケースでは「モデル圏全体 vs モデル圏の対象」という食い違いをうまく調停するメカニズムが存在します。
Algebras-as-Typesの立場、代数的型理論では、代数指標Σに対してモデル圏Mod[Σ]は、Σ代数の圏 AlgΣ です。項モデルの方法を使うと、圏AlgΣには始対象が存在することがわかります。その始対象は始代数と呼ばれます。始対象（＝始代数）は同型を除いて一意的なので、指標Σに1つの代数（代数構造）が対応すると思ってかまいません。
以上の手順で、指標Σと始代数が1：1に対応します。つまり、始代数という典型的な対象を考える限り、「指標が型である」と言っても「モデル圏の対象が型である」と言っても同じことになります。余代数的型理論でも同様で、モデル圏の終対象（終余代数）を考えれば、指標と対象が1：1対応しています。
指標 -- 具体的にはクラスやモジュールのインターフェースが与えられたとき、その意味を始対象または終対象とみなす意味論はタイト意味論（tight semantics）、特定の対象を選ばないで、指標の意味をモデル圏全体だと考える意味論をルーズ意味論（loose semantics）と呼ぶことがあります。モデル圏から特定の対象を1つだけピックアップすることが可能ならタイト意味論が構成できますが、そうでないとタイト意味論は作れません。
「モデル圏全体が型の意味」というのは、確かに茫漠としていて扱いやすくありません。始対象／終対象のような特定対象を選ぶ代わりに、モデル圏に同値関係を入れて縮めてしまうこともあります（「仕様技術への道 -- インスティチューションを縮めてみる」参照）。
あの手この手で圏全体をより小さなモノにしようとしているわけです。ですが、別に小さくしなくてもいいんじゃないか、とも思います。特に手を加えないで、そのまま Categories-as-Types 。まー要するに、あんまり細工をせずにインスティチューションの枠組みで素直に事態を眺めればいいだろうと。-- そんなこと思う昨今。（結論は特になし。）
