次元0 ワイヤー、ケーブル ⊥： 波線 T： 破線 A: 実線 Γ： 実線または幅付き線 次元1 ノード次元1 AND X_{Γ, Σ} ： スワップ Γ # Σ → Σ # Γ Δ_Γ ： 分岐 Γ → Γ # Γ !_Γ ： 削除 Γ → T π^1_{A, B} : 横線 (A, B) → (A) π^2_{A, B} : 横線 (A, B) → (B) ∧_{A, …

指標はラベル〈名前〉の宣言文だけを並べたもの。別名は： セオリー： 指標をセオリーと呼ぶ人がいる。 文脈〈コンテキスト〉： 型理論ではよく使う。特に型シーケントの仮定側を文脈と呼ぶ。 束縛： 型付きラムダリストに現れる宣言の並びは束縛と呼ばれる…

TypeScriptで宣言空間という独特の言葉を使う。「名前空間」と呼ばない理由は： 「名前空間」はファイルとは別なモジュールを意味するので、コンフリクトを避けた。 名前の容れ物というより、名前の分類基準に近い。 宣言された名前がどの種別かは： 変数名…

パッケージマネージャーとビルドツールは必要。 パッケージ直下の階層の存在物はモジュールでいいと思う。モジュールは物理ファイルに対応がわかりやすい。 スケルトンが何であるか？ の位置付けがよく分からない。 ビルドツールとバンドラーの境界線は確か…