まず、次は同義語扱いしたほうがいい。 変数の型宣言 型コンテキスト 0-指標 ポイント1-射だけの1-指標 構造体定義 レコード定義 テーブルスキーマ 例えば、 variable x, y : Real, c : Color type-context {x:Real, y:Real, c:Color} 0-signature _ { 0-mor…

型の圏（複圏、多圏もある）と命題の圏（複圏、多圏もある）との関係。カリー／ハワード／ランベック対応（むしろ、カリー／ハワード／ランベック・フレームワーク）があるので似てる。抽象化すれば同じになる。が、型コンテキストの圏の対象の上に命題の圏…

MEDL（Mathematical Entity Description Lang.）とDIDL（Drawing Instruction and Description Lang.）について。DIDLはある程度は汎用の絵図記述言語。だが、直接的な目的は証明記述。「証明」は曖昧語なので、テクニカルタームとしては導出〈derivation〉…

MP導出の図を向きを変える。 スタックとリストの関係と等式の証明 計算図 リーズニング図 紙芝居方式リーズニング図リーズニング図の同値変形 分岐合流紙芝居方式リーズニング図 線形証明とグラフ証明図とツリー証明図連言リストと宣言リスト、α, β は論域。…