# Sheaf conditions for presheaves of (continuous) functions. #

We show that

`Top.Presheaf.toType_isSheaf`

: not-necessarily-continuous functions into a type form a sheaf`Top.Presheaf.toTypes_isSheaf`

: in fact, these may be dependent functions into a type family

For

`Top.sheafToTop`

: continuous functions into a topological space form a sheaf please see`Topology/Sheaves/LocalPredicate.lean`

, where we set up a general framework for constructing sub(pre)sheaves of the sheaf of dependent functions.

## Future work #

Obviously there's more to do:

- sections of a fiber bundle
- various classes of smooth and structure preserving functions
- functions into spaces with algebraic structure, which the sections inherit

We show that the presheaf of functions to a type `T`

(no continuity assumptions, just plain functions)
form a sheaf.

In fact, the proof is identical when we do this for dependent functions to a type family `T`

,
so we do the more general case.

The presheaf of not-necessarily-continuous functions to
a target type `T`

satsifies the sheaf condition.

The sheaf of not-necessarily-continuous functions on `X`

with values in type family
`T : X → Type u`

.

## Equations

- TopCat.sheafToTypes X T = { val := TopCat.presheafToTypes X T, cond := ⋯ }

## Instances For

The sheaf of not-necessarily-continuous functions on `X`

with values in a type `T`

.

## Equations

- TopCat.sheafToType X T = { val := TopCat.presheafToType X T, cond := ⋯ }