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

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.

-