Sheaf の続き

なんか、ぜんぜんできなくて。で、どうも、Sheaf の定義が違うらしい

Pull back って a b の二つの対象にたいして定義するんだが「任意の a b 全部」って書いてある

a b に対して、pull back が決まるのではなくて「全部の a b 　の組に対して」決まるのか

ところが、それを書こうとすると、任意個の直積を書かないとだめ。Equalizer で書けるとか書いてあるが…

まぁ、pull back をコピペして (a b : I )を引数で入れればいいんだろ?

Lean 4 で書いてあるのもあるっぽい