ステージデザインとシナリオスクリプトで指定すること。 ストーリー〈コース〉の開始ステージ（入り口）と終了（出口）の指定。 各ステージのコンテキスト（予備知識）とスキル（コマンドセット） ステージクリア条件 クリアした後の進行先の選択肢、条件付…

論理的体系のマクロな構造とその学習は、リーズニングゲームで行う。リーズニングゲームは、背景知識／背景スキル〈コマンドセット〉を提供するグリモワ〈仏: grimoire | 魔導書〉と、ゲーム・ストーリーからなる。ゲームストーリーはパッケージとして流通単…

eviは証拠〈evidence〉の略記だとする。命題と証明の圏 $`{\bf Ded}`$ から集合圏への関手が定義できる。 $`P\in |{\bf Ded}| \mapsto \mathrm{evi}(P) := {\bf Ded}(\top, P)`$ $`(f:P \to Q) \text{ in }{\bf Ded} \mapsto \mathrm{evi}(f) := {\bf Ded}(\…

依存型に一般化したカリー同型：$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\In}{ \text{ in } } `$$`\quad \cat{C} \in |{\bf Cat}|\\ \quad A:I \to |\cat{C}|_0 \In {\bf Set}\\ \quad \prod_{i\in I} \ca…

次の同型が成立する。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} }`$$`\prod_{i \in I} {\bf Set}[X, A[i] ] \cong {\bf Bun}[I](X \times I, \sum_I A[\bullet]) \\ \cong {\bf Fam}[I](\mrm{K}^X_I, A[\bullet]) `$名前だ…

まだユルユルな議論なのだが、コンテナの次元UPした概念である2-コンテナとインスティチューションを組み合わせてセオリー論を洗練させられる気がする。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} }`$ コンテナ インスティ…