演繹系（証明系）を、技術者の言葉で語ることが課題。まだ、いろいろと思案中だがね。まず、基本的な態度あるいは視点としては； 演繹系も計算システムであるので、通常のコンピュータシステムやプログラミング言語システム（言語処理系と実行環境）と同じだ…

Bruce Bartlett の "Categorical Aspect of TQFTs"(TQFTはフルスペル) より： Theorem (Reshetikhin and Turaev [89]).Let (C,×, 1, σ, θ) be a ribbon category. Then the evaluation of a ribbon diagram into a morphism in C is invariant under 3d isot…

表題の言葉がいきなり頭に浮かんだ。その状況と理由は … それは後日にする。ニュートンとライプニッツのどっちが先に微積分を発見したのか？ という話があるが、歴史的に早い遅いはどうでもいい（差があっても僅差だろう）として、記号法の便利さは圧倒的に…

1次元ベクトル空間の圏に、零空間を入れても圏になる。0と1に掛け算を入れた代数系の圏化／線型化かな？零空間は1個しかないと思ってもいいし、無限にあると思ってもいい。射は同型か零写像しかない。

ボブクックが本を編集しているらしい。 http://golem.ph.utexas.edu/category/2008/09/new_structures_for_physics_ii.html バエズ／ステイの論文がリバイスされている。 http://math.ucr.edu/home/baez/rosetta/rose4.pdf 50ページからが「計算」の章。P.50…

林晋さんの論理の本（オーム社だったか）に、カリー／ハワード対応が載っていたような気がする。この本ないなー。どこだ？