前回の圏論勉強会で出た話の備忘録。
今やってるテキストに、"Cartesian category"(カルテシアン圏?とかデカルト圏とか。以下CC)なるものが出てきます。これは、λ計算が成すような Cartesian closed category (カルテシアン閉圏とかデカルト閉圏とか。以下CCC)から、冪(≒関数の型)を抜いたような圏なんですけども。
じゃあその closed って何やねん、という話になりまして。いろいろ話した結果、どうもこういう事らしいです。
ゆえに前順序におけるモナドはちょうどにおける閉包演算(closure operator)となる。すなわち任意のについてとが成り立つ単調関数である。
CCCに関して言えば、CCに任意の対象に対して冪が入ると、元々あった、直積を作る関手に対して右随伴の関手となります。そうすっと、結果として2つの関手の組み合わせがモナドを形成します。そのモナドが作れることが、CCCの真ん中のC (closed) を意味するっぽい、です。
ちなみに、上記の引用文で x ≦ tx が unit( Haskell でいう return )、t(tx) = tx が join( Haskell の Monad.join )に相当するってことですね。
追記。closed categoryのちゃんとした定義あった。でもココロは上のような理解でいいんだろうと思われ。
閉圏 (closed category)Vは、対称モノイダル圏で、−□b: V → V の形の各函手が特殊な右随伴 ()b: V → V を持つようなものである。