実線は望ましい対応。点線は連想や混同。
$`\xymatrix{
\text{型構成子}
&\text{論理演算} \ar[l]
\\
\text{型}
& \text{命題}\ar[l] \ar@{.>}[d] \ar@{.>}@/^/[dd]
\\
\text{関数} \ar@{.>}[d] \ar@{.>}@/_/[dd] \ar@{.>}@/_1.5pc/[ddd]
& \text{定理}\ar[l] \ar@{.>}@/^1.5pc/[ddd]
\\
{\text{関数宣言}}
& \text{公理} \ar[l]
\\
\text{計算}
& \text{証明} \ar[l]
\\
\text{関数定義}
&{定理記述} \ar[l]
\\
\text{プロファイル}
&\text{シーケント} \ar[l]
\\
\text{データ}
& \text{証拠, 証書} \ar[l]
}`$
以下でうまくいくか？
$`\xymatrix{
\text{型}
& \text{命題}\ar[l]
\\
\text{型定義}
& \text{命題定義}\ar[l]
\\
\text{関数}
& \text{定理}\ar[l]
\\
{\text{外部関数}}
& \text{公理} \ar[l]
\\
{\text{外部関数宣言}}
& \text{公理記述} \ar[l]
\\
\text{関数定義}
&{定理記述} \ar[l]
}`$
それとは別に、命題が述語関数として関数の一部に埋め込まれる現象があり、これも混乱のもと。どうすべきか？
- 命題は型である。
- 命題は関数である。
「命題である関数＝述語」を型ファミリーに持ち上げる話が必要か？
