*-as-Typesパラダイム

セオリー論 型理論
  1. Sets-as-Types, Functions-as-Terms
  2. Algebra-as-Types, Morphisms-as-Terms
  3. Coalgebra-as-Types, Morphisms-as-Terms
  4. Categories-as-Types, Functors-as-Terms
  5. Propositions-as-Types, Proofs-as-Terms

Sets-as-Types と (Co)Algebras-as-Types は、単純型＝ソートと構造型〈複雑型〉として説明できる。単純型の圏の上の具象圏（忘却関手付き圏）として構造型が定義できる。忘却関手達のグラフは型階層を与える。

Categories-as-Types は、圏という代数を Algebrs-as-Types で解釈すれば、構造型の一種になるが、通常は 圏＝種＝型の型と考えて 2-型の理論を展開する。2-型の2-指標をドクトリンと呼ぶ。

Propositions-as-Types は、自然演繹を使う場合とシーケンとを使う場合ではだいぶ違う。2つの定式化の関係をハッキリとすべき。