「構文付き変換手インスティチューション 1/n」において、半具象インスティチューション〈semi-concrete institution〉という言葉を出しました。インスティチューション理論における指標の圏〈category of signatures〉やモデル関手〈model functor〉は、公理的・天下りに与えられるので、まったく具体性を持ちません。（完全に具体的でなくても）もうちょっと具体的に規定されたインスティチューション、という意味で「半具象インスティチューション」と言ったのです。$`\newcommand{\cat}[1]{\mathcal{#1}}`$
型理論／型システムのモデルである圏は、半具象インスティチューションの指標の圏として使えるのではないか、と思っています。型理論／型システムのモデルである圏には次のようなものがあります。
- 属性付き圏〈category with attributes | CwA〉
- ファミリー付き圏〈category with families | CwF〉
- ディスプレイ射のクラス付き圏〈category with display maps | CwD〉
- コンテキスト圏〈contextual category〉／C-システム〈C-system〉
- 包括圏〈comprehension category〉
これらについては、次のnLab項目に要領良くまとめられています。
次の論文も全般的な状況を知るのに役立ちます。
- [Zha21-22]
- Title: Type theories in category theory
- Author: Tesla Zhang
- Submitted: 28 Jul 2021 (v1), 4 Apr 2022 (v5)
- Pages: 47p
- URL: https://arxiv.org/abs/2107.13242
上に列挙した一連の圏の種別を総称して型理論的圏〈type-theoretic categories〉と言うことにします。型理論的圏はどれも、対象がコンテキスト（と呼ばれる何か）である圏に上部構造が載った形をしています。型理論的圏の下部構造を形成する圏をコンテキストの圏〈category of contexts〉と呼ぶことにします。コンテキスト圏〈contextual category〉と紛らわしいですが、コンテキスト圏は型理論的圏の一種で、“コンテキスト圏のコンテキストの圏”〈the category of contexts of a contextual category〉があります。
$`\cat{C}`$ を型理論的圏のコンテキストの圏とします。圏 $`\cat{C}`$ を、半具象インスティチューションの指標の圏〈category of signatures〉として使うのが良さそうです。つまり、型理論のコンテキストとインスティチューション理論の指標（のより具体的なバージョン）を同一視することになります。
型理論的圏のコンテキストの圏の射は代入〈substitution〉と呼ばれます。代入はコンテキスト射〈context morphism〉と呼んでもかまいません。コンテキストとコンテキストを繋ぐ射ですから。一方、インスティチューションの指標の圏の射は指標射〈signature morphism〉です。
コンテキストと指標を同一視したのだから、コンテキスト射と指標射も同一視すればいいでしょうか？ どうも具合が悪い。射の方向が逆なんですよね。インスティチューションの意味での“指標と指標射からなる圏”を $`\cat{S}`$ とすると、次のような関係があるようです。
$`\quad \cat{S} = \cat{C}^\mathrm{op}`$
互いに反対圏なのです。
型理論的圏のコンテキストの圏 $`\cat{C}`$ の上には構造が載ります。指標の圏 $`\cat{S}`$ がコンテキストの圏 $`\cat{C}`$ の反対圏だとすると、指標の圏には双対的な構造が載ります。この双対的な構造が、半具象性を提供してくれそうです。
[追記]次の論文も型理論の概観を得るには良さそうです。
- [Cap13-]
- Title: Type Theory through Comprehension Categories
- Author: Paolo Capriotti
- Date: July 12, 2013
- Pages: 46p
- URL: https://paolocapriotti.com/assets/report-2013.pdf
[/追記]
