Functors as Types

型の意味は関手で、項の意味は自然変換だと考える。型である関手の定義域は、「スキーマ、シェープ、指標」などと呼ばれる。型の定義域の全体はまた圏で、スキーマ圏、シェープ圏、指標圏などと呼ぶ。インスティチューションや導来子との類似性がある。

• 導来子の図式の圏 → スキーマ圏、シェープ圏、指標圏
• 導来子の値 → 指標に対するモデル圏
• 導来子の単位圏での値 → モデルのアンビエント圏

おそらく、総称（多相）の説明になるだろう。