コマンドは、先頭が動詞原型または動詞過去分詞形、それに続いてキーワード目的語名詞が続いてもいい。apply, make conjunction, found inconsistency など。「命題 by 根拠名詞 引数並び」でも証明が書けるとする。以下、根拠名詞とコマンド動詞の対応表。 …

命題、証明、規則をそれぞれ0-射、1-射、2-射の意味で使う。 公理 公理証明 ax_A : * -> A * ----[ax A] AAx⊆|C| なので、Axは命題の集合として与えられるが、それはデカルト閉圏の特殊事情で、一般には、 a : X -> A X ---[a] Aつまり、Ax⊆Mor(C)。Axはどん…

A1, ..., Anを仮定（assume）してBを結論（conclude, entail, result, produce, show）する証明があるとき、その証明内で使っている暗黙の知識がある。これを証明の文脈とか環境と呼ぶ。で、文脈とは正確には何か？ が大問題。それと、トンネル論法（コンパ…

Webフロントエンドでの話 - 檜山正幸のキマイラ飼育記 メモ編 の続き。browserify, babele, webpackとか。 babelはトランスパイラである、と。で、browserifyはトランスパイラとは違うのか？ browserifyは、依存性を分析してブラウザー向けに変換するのかな…