Sheaf

なんか、qemu mc6809 の方が「やる気的に」に行き詰まってるので

圏論の Sheaf の方に手をつけてみました

なんだって?

　A Presheaf on X is a contravariant functor from O(X) to Sets.

簡単じゃん

　 presheaf : {P : HOD} (TP : Topology P) → Set (suc (suc (suc n)))
　 presheaf {P} TP = Functor (Category.op (OSC TP)) (Sets {n})

OSC は、

　SetsC : Category (suc n) n Level.zero
　SetsC = record { Obj = HOD
　 ; Hom = _⊆_
　 ; Id = λ {a} {e} ae → ae
　 ; _o_ = λ a b → λ x → a (b x)
　 ; _≈_ = λ a b → ⊤
　
　OSC : {P : HOD} (TP : Topology P) → Category _ n Level.zero
　OSC {P} TP = FullSubCategory SetsC (λ x → OS TP ∋ x )

簡単じゃんってところなんだが、Sheaf の条件が、結構、複雑

pointwise がどうこうとか、なんなんだ〜