スパイダー亜圏
亜圏(categoroid)って言葉はやっぱり圏もどきという意味。トレース付き圏とそこから作ったコンパクト閉圏を一緒に計算する計算デバイスとしてスパイダー亜圏ってのを考えることにした。ネーミングはどうにもアレだが、いい名前が思い浮かばない。
スパイダー亜圏Cには、Ob(C), Mor(C), dom, cod, idなどがあるが圏にはなってない。演算は、縦結合;、対象モノイド積+、トレース、横結合* の4種類。圏とほとんど同じだし、意味論は圏なんだが、計算は微妙にずれている。ズレの原因は、ボックスのポート(ピン)に名前が付いているから。よって、リネームという操作とリネーム同型が本質的に重要な概念になる。
余対角=加法と単位がついた対象モノイド圏が舞台。いずれちゃんと書かないとな。