$`\newcommand{\mrm}[1]{ \mathrm{#1} }`$
- 0-指標の場合は関数の定義
- 1-指標の場合は関手の定義
- 型理論： 証拠〈witness〉付き型判断（コンテキスト＝名前付き指標）
- 論理： 証明
- プログラミング：ソフト実装、アダプター
手続きの域は指標だが、ソース・コンテキストとも呼ぶ。余域はターゲット・コンテキスト。
型理論では手続き射のプロファイルを $`\Gamma \vdash \Delta`$ と書き、手続き／手続き定義を判断の証拠と呼ぶ。
モデルをハード実装、手続きをソフト実装と呼んで、論理の記号を借りるとよさそう。
- $`M \models \Sigma`$ 指標のモデル〈ハード実装〉である。
- $`M \in |\mrm{Model}(\Sigma)|`$ 上とまったく同じ意味。
- $`\Delta \vdash \Sigma`$ 指標は構成可能、導出可能〈derivable〉である。
- $`\Delta \vdash p: \Sigma`$ 指標の構成手続き〈ソフト実装〉である。
- $`p: \Delta \to \Sigma \text{ in } \mrm{Proc}`$ 上と同じ意味。
相対指標（指標テレスコープ）と指標フラグメントの概念を使うと、インスティチューションやπインスティチューションを再現できるのではないか？ $`\models`$ と $`\vdash`$ の使い方が抽象論理／抽象モデル論を構成する。
