何日か前（2005-04-12, 2005-04-13）、indexed categoriesについて触れたことがありますが、僕は、型（タイプ）とは結局、indexed category（またはfibred category）だろうと思っています。つまり、types as indexed-categories という立場ですね。
ただし、"types as indexed-categories"解釈を採用するのは、“パラメータ付きオブジェクト仕様”としての型のときであって、あらゆる型を"types as indexed-categories"の観点で見るわけではありません。次のような使い分け（というか“考え分け”）をしてます。
- 基本型のとき：types as sets、またはtypes as algebras
- 簡単なオブジェクト実装型のとき：types as coalgebras
- 複雑なオブジェクト実装型のとき：types as hidden-algebras
- パラメータなしのオブジェクト仕様型のとき： types as categories、または（同じことだが）types as theories
- パラメータ有りのオブジェクト仕様型のとき： types as indexed-categories、または（同じことだが）types as dependent-theories*1
…というような話を日記エントリ内でザッと説明しようかな、と思いましたが、さすがに長くなりそうなので、キマイラ・サイトの記事にします。
なんか、書きかけの記事がたまってきたなー。
*1:relative theoriesとかparameterized theoriesともいいます。
