github と HTML

元の github は、HTML が結構排除されてて。でも、agda は HTML生成機能があって、わりときれい。

で、どこに置くのかと探したんですが、github.io を使うらしい。特定の名前でおけばいいわけね。

元のと連携する ci ぐらい書きたいが、まぁ、いいかな。

Topology の方は、compact と finite intersection の同値までできました。チコノフの定理まで、あと少しだな。

https://shinji-kono.github.io