まず、次は同義語扱いしたほうがいい。
- 変数の型宣言
- 型コンテキスト
- 0-指標
- ポイント1-射だけの1-指標
- 構造体定義
- レコード定義
- テーブルスキーマ
例えば、
variable x, y : Real, c : Color
type-context {x:Real, y:Real, c:Color}
0-signature _ {
0-mor x in Real
0-mor y in Real
0-mor c in Color
}
1-signature _ {
1-mor x : 1 → Real in Set
1-mor y : 1 → Real in Set
1-mor c : 1 → Color in Set
}
struct ColoredPoint {
Real x,
Real y,
Color c
}
record ColoredPoint {
x: Real,
y: Real y,
c: Color
}
schema ColoredPoint {
x : Real,
x: Real,
c: Color
}ソート、ポイント1-射、変数型選言、法則からなる定義を伝統的指標と呼ぶ。
参考： U+21D2 ⇒ RIGHTWARDS DOUBLE ARROW, U+21D0 ⇐ LEFTWARDS DOUBLE ARROW
trad signature Monoid {
sort U
point m:[U ⇐ U×U]
point e:U
variable x, y, z : U
law assoc :: m(m(x, y), z) = m(x, m(y, z))
varible x : U
law lunit :: m(e, x) = x
law runit :: m(x, e) = x
}伝統的指標は、無法則指標と型コンテキストと型コンテキスト上の論理式〈命題〉に分解できる。
無法則指標に対して、それから生成される型と関数の圏、型コンテキストと置換の圏が決まる。法則の命題は、ハイパードクトリンの生成系になる。
- assoc-prop ∈ Prop[{x, y, z : U}]
- lunit-prop, runit-prop ∈ Prop[{x : U}]
デカルト・ハイパードクトリンに対する演繹システムは、次の構文要素を持つ。
- 型項
- 関数項、複関数項、多関数項
- 型付き変数と型コンテキスト
- 置換〈代入〉射
- 命題項＝論理式
- 導出項＝マクロ導出
- リーズニング項＝マクロリーズニング
Γ, Σ, Δ などは型コンテキストを表す。置換射〈substitution〉は S:Γ → Σ というプロファイルを持つ、これは導出とシーケントではない。
置換射は、反変的な翻訳関手〈translation functo〉 S* = (-)[S] を誘導する。翻訳関手、翻訳関手の対象パート／射パートを置換〈代入〉と呼ぶことがある。
限量子は翻訳関手の左右の随伴パートナー関手として定義される。限量子は命題と導出の圏のあいだの関手である。
それと、$`\Gamma \mid \Theta \vdash \psi`$ 形式のシーケント（導出のプロファイル）において、
- $`\Gamma`$ は型コンテキスト〈type context〉
- $`\Theta`$ は命題コンテキスト〈proposition context〉
- $`\psi`$ はターゲット命題〈target proposition〉
型コンテキストで宣言された自由変数しか命題内で使えない。
例：
$`\quad \{x:{\bf N}, y:{\bf N} \} \mid (\text{odd}(x), \text{odd}(y)) \vdash \text{even}(x + y)`$
