a function of a dependent type, a section, a sheaf

Question

I have defined this simple sheaf. Take $E:set, B:set, p:E\to B$. Let $P(B)$ be a set of subsets of $B$. Let $S$ be the set of sections of $p$. Let $F$ be a contravariant functor from $P(B)$ as a poset category to $Set$ which sends:

• objects: $B'$ to ($S$ with elements restricted to $B'$);
• morphisms: an inclusion to the restriction of functions;

and the discrete topology on $P(B)$ and obvious gluing. I call $F$ the “sheaf of sections”, is there a standard name? Was anybody studying it? (Perhaps it is too simple.) A motivation is that sections can be identified with functions of a dependent type which generalize typed tuples.

Answer 1

If I read that right, you're just looking at the sheaf of sections of E->B, with E, B sets, B with topology P(B) [If by P(B) you meant the power set, the discrete topology]. I don't think these examples are particularly popular, but you can treat them like any other sheaves of sets (see, perhaps, MacLane-Moerdijk, Sheaves in Geometry and Logic).