Sheaf

まだ、 Adjunction ((topology X)ᵒᵖ → Sets ) ( top / X ) と戦ってるわけですが、

　ΓとLは、だいぶできた

なんだが、「Finally, it is easily verified that ...」が、まったくわからん

この Finally が笑えるのは、Lを作ってるところの Finally なので、さらに、自然変換二つと、その等式二つが残ってるわけ

でも、Agda で書けるので「忘れることはない」。「今まで書けたところは、そのまま残っていて使える」わけね

でも、これプロシンで発表する話でもないしなぁ。役に立つなら話は別なんですが

まぁ、まったくわからんといっても、nat : F → G から、L(F) → L(G) は構成できて、top / X の射の条件である射を作ってるところ

そのうちできるはずです