論文を読んだわけではないので、推測だけども、Joyalらが、traced monoidal categoryを導入した動機というのは、braided monoidal categoryの場合、ブレイド群からへのmappingが存在するので、それをtraceでEnd(I)の元に落とすことで、結び目の不変量が得ら…

Traced Premonoidal Categoriesを読んだ。ある種のモノイダル圏では、traceと不動点作用素(正確には、parametrized fixpoint operatorでConway作用素と呼ぶらしい)が本質的に同じものだという、なんか不思議な話。元々は、traced monoidal categoryの定義を…

Constructive Category Theory圏論を知ってれば、Coqの記号がキモイ以外は読みやすい論文だった。一般の型に属する値は等しいかどうかの判定が可能とは限らないので、ある型とその型の上の同値関係のペアとしてSetoidというのを導入する。同値な要素は、等し…

とりあえず、MLのモジュール・システムでもfunctorという用語が使われてること、そいつが何か圏論に由来するらしいことは分かった。OcamlのmoduleとMLのmoduleって多分一緒なんかな〜 MLモジュールシステムを圏論的に理解しようとしてる論文 A Category-Theo…

LFixとGFixが、始代数と、終余代数を与えるなら、LFix fからGFix fへの射を作る、自然で簡単な方法が存在する。これにすぐ気付かないのは、アホだな私Fを適当な圏の自己関手で、F始代数とF終余代数が存在するものとして、(T,in)をF始代数とすると、inは同型…

http://citeseer.ist.psu.edu/bierman95what.html(直観主義)線形論理の圏論的モデルには、linear category("Gang of four" model)を使うものと(new-)Seely categoryを使うものの見かけ上異なる2種類あって互いに同値(linear categoryの定義は、任意の有限積…

・圏CPOの定義。完備半順序集合(cpo=任意の上昇列が最小上界を持つような半順序集合)とその間の連続関数(多分順序と極限を保つという意味。位相空間の開集合の全体が半順序集合になるというとこから来てる名前なんでしょう)を射とする圏。最小元を持つ場合は…

というような話がリストでしか言えないなら、新しくデータ型を作るたびに、ルールを発見せねばならず、大して面白くもないんだけど、foldとかbuildとかaugmentは、圏論的背景を持ってて、Haskellの他のデータ構造でも使えるという話なので、素晴らしいかもし…

まあ、こんな構成は、とっくの昔に誰かがやってると思うけど、関手Fの不動点を構成する方法として、適当な対象Xに関手Fをどんどん適用していって、極限取ればいいよね、という素朴な思いつきがある。別に関手でなくて、関数でもよくやる。極限がいつ存在する…