Heap (груда)とgroup (группа)

heapというものがあって、heapから任意の元eを選んだら、eを単位元とする群が作れるらしいです。heapの圏から群の圏への関手を定義しようと思ったら、構成手法によってはpointed heapから成る充満部分圏を考えないといけないかもしれませんし、選択公理を仮定するならinhabitedでもいいかもしれません。ちなみに、pointed heapについて考えたときに射がbase pointを保存することまで要求してしまうと、群の圏と圏同値になってしまう予感がします。

contextは5.4節の初めまで来ました。5章の中でも特に面白くなってきましたね。Monadic categoryが良い性質を持っているのを見ると嬉しい気持ちになります。

この記事は個人サイトでも読めます。