「続・カリー／ハワード／ランベック対応の辞書」にて： 圏論では、射のあいだの等式的関係、例えば $`\langle f , g \rangle; \pi_1 = f`$ などが重要ですが、論理ではあまり言及しません。分野ごとに、興味のあり方や価値観が違うからでしょう。 論理にお…

現状の証明支援系〈proof assistant〉について、僕はしょっちゅう愚痴と文句を言っています（twitterでぼやいたりしてる）。大きな不満点は、フォワード・リーズニングの対話的サポートがまったくない点です。不便だし面白くない。内容： 証明ソフトウェアの…