Sheaf の記述

「It is easily verifed that Γ p is a sheaf」は終わって、Lを書いている最中。たくさん出てくるのが集合であることを示しているところ

まぁ、最初の Functor のFObjが集合なのは仮定するわけだけど

でも、その 「It is easily verifed that Γ p is a sheaf」なんだが、それまでの準備に 600行。そして、sheaf であることを示すのに200行

そもそも sheaf を示すのに関数三つ作らないとだめで、そのひとつは連続写像であることも示すことになる

まぁでも、Zornの補題の時よりはましな気がする。量的には既におなんじくらいだけど、Zorn の時は、かなり書き直したので

これ、Agda 抜きだと、無理だっただろうなとは思う。覚えてられない感じ