南極

github のあれですが、結構な比率で取ってるらしく自分のも一つ引っかかりました。圏論の方が量は多いんだが、集合論の方ね。

うちの卒業生でも github 使ってるのは多いので、そこそこ引っかかってるみたいね。

fork は元のしか取らない方針なのかな。

集合論の方は Generic Filter の定義はできたので、いろいろやる部分があるのだが、取りあえず集合の自然数とAgdaのNatの変換の iso を書くので

いつもの依存性のある項の置換で引っかかってます。あれ、なんか統一的な解法ないのかな。