久しぶりに圏論

なんか休みになると Agda に触っている感じ。コンパイラのバグが厄介そうなので、ちょっと逃避ですね。

今回のお題は、

Complete Category が initinal object を持つ iff Preinitial Full Subcategory

ですね。フロイトの随伴関手定理の補題らしい。いつもの Higher order categorical logic の0章。

相変わらず、そっけない証明が記述されているだけなんですが、

Subcategory は A から A への関手があれば良い
Full は射が全部あるってことなので、関手の逆射があれば良い

というのを3月の辺りに書いていて、それがばっちりだったので、割とすぐにできました。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/61550782be4a/freyd.agda