2021-05-07から1日間の記事一覧

「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ六「等号の規則」「仮定付判断と代入規則」（復習編）

お休みを挟んでこれの復習編。等号の規則これは導出可能規則と言ってもよさそうだけど、どうも導出体系ではないという点が重要そうなのでそうは言えない。特にカノニカルな要素を得る計算というのはあまりフォーマルに導入されていない。が集合だと言って…