ビンゴ！ 「インスティチューションの“指標の圏”の具体化として、型理論的圏の反対圏をとればいいだろう」と見当をつけていたのですが、アタリだったようです。型理論的圏は、拡張包括構造を持ちます。拡張包括構造を持つ圏上の、プルバック四角形（コスパンの極限）を保つ余インデックス付き圏は、自動的に、反対圏上にインスティチューション構造をもたらします。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\In}{\text{ in }}
\newcommand{\Imp}{\Rightarrow }
\newcommand{\Iff}{\Leftrightarrow }
`$
「指標の圏はコンテキストの圏の反対圏」より：
インスティチューションの意味での“指標と指標射からなる圏”を $`\cat{S}`$ とすると、次のような関係があるようです。
$`\quad \cat{S} = \cat{C}^\mathrm{op}`$
互いに反対圏なのです。
型理論的圏のコンテキストの圏 $`\cat{C}`$ の上には構造が載ります。指標の圏 $`\cat{S}`$ がコンテキストの圏 $`\cat{C}`$ の反対圏だとすると、指標の圏には双対的な構造が載ります。この双対的な構造が、半具象性を提供してくれそうです。
型理論的圏〈type-theoretic category〉は、コンテキストと呼ばれる対象達の圏 $`\cat{C}`$ で、なんらかの拡張包括構造〈extension-comprehension structure〉を持っています（「拡張包括構造のもうひとつの定式化」参照）。コンテキスト〈対象〉拡張の演算を '$`\cdot`$' で表すことにします。コンテキスト拡張に伴う標準射影射〈canonical projection morphism〉は次のようです。
$`\quad \xymatrix{
X\cdot A \ar[d]^{\rho^{X, A}}
\\
X
}\\
\quad \In \cat{C}
`$
任意の射 $`f:Y \to X \In \cat{C}`$ によりコスパンを作ります。
$`\quad \xymatrix{
{}
& X\cdot A \ar[d]^{\rho^{X, A}}
\\
Y \ar[r]_f
& X
}\\
\quad \In \cat{C}
`$
$`\cat{C}`$ 上の拡張包括構造により、このコスパンから、プルバック四角形（標準プルバック四角形）を一意的に構成・選択できます（「拡張包括構造のもうひとつの定式化」参照）。
$`\quad \xymatrix{
Y\cdot f^* A \ar[r]^{f^\uparrow} \ar[d]_{\rho^{Y, f^* A}}
\ar@{}[dr]|{\text{p.b.}}
& X\cdot A \ar[d]^{\rho^{X, A}}
\\
Y \ar[r]_f
& X
}\\
\quad \In \cat{C}
`$
$`f^*`$ は、「拡張包括構造のもうひとつの定式化」における $`\mrm{Step}(f)`$ の略記です（アスタリスクじゃないほうが良かった気がするけど）。$`f^*`$ は、反変関手〈前層〉 $`\mrm{Step}`$ が $`f`$ に作用して生まれた関数〈集合圏の射〉です。
今、$`F:\cat{C} \to {\bf Cat}`$ を、厳密な（スードではない）共変関手（反変関手ではない）とします。$`F`$ は、$`\cat{C}`$ 上の余インデックス付き圏〈coindexed category〉ということです。さらに、関手 $`F`$ はプルバック四角形を保つとします。$`\cat{C}`$ 内のプルバック四角形は、$`{\bf Cat}`$ 内の厳密プルバック四角形（四角形が厳密可換であるペースティング図）に移されるとします。これは、$`F`$ に対する連続性条件〈極限保存条件〉です。
上記の標準プルバック四角形を $`F`$ で移したプルバック四角形は次のようです。四角形は厳密可換なので $`\text{strict}`$ を添えています。
$`\quad \xymatrix{
F(Y\cdot f^* A) \ar[r]^{F(f^\uparrow)} \ar[d]_{F(\rho^{Y, f^* A})}
\ar@{}[dr]|{\text{strict p.b.}}
& F(X\cdot A) \ar[d]^{F(\rho^{X, A})}
\\
F(Y) \ar[r]_{F(f)}
& F(X)
}\\
\quad \In {\bf Cat}
`$
このセッティングにおいて、関手 $`F`$ はインスティチューション理論の充足関係〈satisfaction relation〉の同値性を満たします。まずは充足関係を定義する必要があります。対象 $`X`$ 上の充足関係は '$`\models_X`$' という記号で書きます。
$`\cat{C}`$ の対象〈コンテキスト〉$`X`$ 、拡張ステップ（型理論の言葉なら“型”）$`A`$ 、そして $`F(X)`$ の対象（インスティチューション理論の言葉なら“モデル”） $`M`$ に対して $`M \models_X A`$ という関係を定義します。証拠〈witness〉 $`M'`$ を含めた充足関係を先に定義します。
$`\text{For } X\in |\cat{C}|\\
\text{For } A\in \mrm{Step}(X)\\
\text{For } M\in |F(X)|\\
\text{For } M'\in |F(X\cdot A)|\\
\quad\: M \models_X A \text{ by }M'\\
\: :\Iff\\
\quad \: F(\rho^{X, A})(M') = M
`$
証拠 $`M'`$ が存在することを単に $`M \models_X A`$ と書きます。
$`\text{For } X\in |\cat{C}|\\
\text{For } A\in \mrm{Step}(X)\\
\text{For } M\in |F(X)|\\
\quad\: M \models_X A\\
\: :\Iff\\
\quad \: \exists M'\in |F(X\cdot A)|.\, F(\rho^{X, A})(M') = M
`$
充足関係の同値性とは、次の命題です。
$`\text{For } X, Y\in |\cat{C}|\\
\text{For } f: Y \to X \In \cat{C}\\
\text{For } N \in F(Y)\\
\text{For } A \in \mrm{Step}(X)\\
\quad F(f)(N) \models_X A \Iff N \models_Y f^* A
`$
$`N \models_Y f^* A \Imp F(f)(N) \models_X A`$ の方向は、$`N \models_Y f^* A`$ の証拠 $`N' \in |F(Y\cdot f^* A)|`$ を取って、先のプルバック四角形可換図式のなかで追いかけるだけで示せます。このとき使うのは、四角形の可換性だけで、プルバックであることは特に使いません。
逆方向の $`F(f)(N) \models_X A \Imp N \models_Y f^* A`$ を示すにはプルバックであることを使います。$`F(f)(N) \models_X A`$ である証拠を $`M' \in |F(X\cdot A)|`$ と置きます（$`F(f)(N) = M`$ のつもり）。対象 $`N`$ や $`M'`$ を、自明圏 $`{\bf I}`$ からの関手だとみなして、次の図式を描きます。
$`\quad \xymatrix@R+2pc@C+1pc{
{\bf I} \ar@/_1pc/[ddr]_{N} \ar@{.>}[dr]|{?} \ar@/^1pc/[drr]^{M'}
& {}
& {}
\\
{}
& F(Y\cdot f^* A) \ar[r]^{F(f^\uparrow)} \ar[d]|{F(\rho^{Y, f^* A})}
\ar@{}[dr]|{\text{strict p.b.}}
& F(X\cdot A) \ar[d]|{F(\rho^{X, A})}
\\
{}
& F(Y) \ar[r]_{F(f)}
& F(X)
}\\
\quad \In {\bf Cat}
`$
四角形がプルバックであることから、疑問符が付いた射が一意的に存在するので、それを $`N'`$ と置きます。次を満たします。
$`\quad F(\rho^{Y, f^* A})(N') = N
`$
言い換えると、
$`\quad N \models_Y f^* A \text{ by }N'`$
証拠 $`N'`$ が存在するので次が言えます。
$`\quad N \models_Y f^* A`$
以上で、$`F(f)(N) \models_X A \Imp N \models_Y f^* A`$ が示せました。
以上の議論を、反対圏 $`\cat{S} = \cat{C}^\mrm{op}`$ 上に移しましょう。反変関手〈前層〉 $`\mrm{Step}`$ は共変関手〈余前層〉に変わります。共変関手となった $`\mrm{Step}`$ が、インスティチューションの文関手〈sentence functor〉となります。共変関手だった $`F`$ は反変関手になります。反変関手となった $`F`$ が、インスティチューションのモデル関手〈model functor〉となります。
反対圏 $`\cat{S}`$ 上では、$`f^* A`$ を $`f_* A`$ と書くことにして、$`F(f)(N)`$ を $`f^* N`$ と書くことにします。すると、充足関係の同値性は次の形になります。
$`\quad f^* N \models_X A \Iff N \models_Y f_* A`$
インスティチューションの公理です。この公理は、指標の圏として型理論的圏（拡張包括構造を持つ圏）をとれば示せるのです。つまり、型理論的圏があれば、それから（モデル関手を追加して）インスティチューションを構成できます。
半具象インスティチューション〈semi-concrete institution〉という枠組みにおける“半具象指標の圏”として、型理論的圏がうまいことフィットしてくれます。
