米田にすべてを任せてみれば、よかったりしないかな

明示的構成ばかりを定義として使うと、証明のときに大変だと気づきました。関手性や自然性を何度も何度も証明しなきゃいけなくなり、とてもやってられないのです。たとえば元の圏は米田埋め込みを使ったコンマ圏と同値らしいので、今度からはもうちょっと抽象的な方法で圏を作るようにしてみます。そうすれば多分米田で殴っていけばなんとかなるんじゃないかと思います。圏論初心者らしい所が出てしまいました。

2つの圏が弱同値であるというのが、対象について本質的に全射な充満忠実関手が存在することなのか、それともそういった関手が別の圏からそれぞれの圏に向かって存在してspanを構成することなのか、どっちなのか良く分からなくなりました。nLab的には後者らしいのですが、モデル圏に詳しくないので何故spanが出てきていいのかが分かりませんでした。もちろん後者の方が対称的で良い定義に見えますが、それがモデル圏的にどう正当化されるのかを知りたいと思いました。

そういえばcontextはモナドの章まで下見を終えました。あとはKan拡張の章が残っているのですが、これについては学び直す以前にそもそも定義を軽く知っている程度でほとんど何も知らないので、また別のプロジェクトとして後回しにします。

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