Sheaf

まだ、やってるんですが、

Γ : Functor ( top / X ) (HOD-OSCA (topology X) )

は、できたので反対側

L : Functor (HOD-OSCA (topology X) ) ( top / X )

をやってるんだが、位相空間を作らないといけない

それは関数の定義域の制限のFunctorの同値類でみたいな話

有限な ∩ と和集合ができればよいんだが、難航してたんだが

　　Functorだけでなく、その元になる関数に well defined な仮定がある

らしく、

　 FO-wld : (F : Functor OX HODSets) → Set (suc (suc n))
　 FO-wld F =　{a b c d : Obj OX}
　　　 → (b⊆a : SObj.s b ⊆ SObj.s a)　→ (d⊆c : SObj.s d ⊆ SObj.s c)
　　　 → {x y : Ordinal} → (ax : odef (FObj F a) x)　→ (cx : odef (FObj F c) y) → x ≡ y
　　　 → Func.func (FMap F {a} {b} b⊆a ) ax ≡ Func.func (FMap F {c} {d} d⊆c ) cx

の仮定を入れるとできるっぽい。でも、有限な ∩ の4つの方向の一つができただけなので、まだ、先が長い

でも、「なにやってるのか」を人に説明するのは無理っぽいので、プロシンには出さないつもりです