Shaef と Agda

Adjunction (HOD-OSCA (topology X) ) ( top / X )

ですが、なんと、一通り書けて、なんでΓの対象が Sheaf になるのかもわかった。

　連続写像の値域の制限ってだけ

なのを、圏とか トポロジーとかSlice圏とか、関手とか、Contravariant とかで難しく書いてあるだけね

なんだが、

　残ってる穴を埋めにいくと、agdaが止まらなくなる

関数が同値なのはすべての値について一致を調べれば良いだけなんだが、そこで止まってしまう

じゃぁ、サーバ側で動かすかと思ったら、既に Agdaのversionが古い。おおい〜

なんか、チェックに時間かかる部分をさぼる方法があったような気がするんだが…

まぁ、もう少し埋めて、それから別なものかな。C-Monoid が面白そう