Commit 2020-08-16 06:05 3c2ed2aeView on Github →
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