feat(topology/sheaves): construct sheaves of functions (#3608)

Sheaf conditions for presheaves of (continuous) functions.

We show that

• Top.sheaf_condition.to_Type: not-necessarily-continuous functions into a type form a sheaf
• Top.sheaf_condition.to_Types: in fact, these may be dependent functions into a type family
• Top.sheaf_condition.to_Top: continuous functions into a topological space form a sheaf