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.