feat(topology/sheaves): the sheaf condition (#3605)
Johan and I have been working with this, and it's at least minimally viable.
In follow-up PRs we have finished:
* constructing the sheaf of dependent functions to a type family
* constructing the sheaf of continuous functions to a fixed topological space
* checking the sheaf condition under forgetful functors that reflect isos and preserve limits (https://stacks.math.columbia.edu/tag/0073)
Obviously there's more we'd like to see before being confident that a design for sheaves is workable, but we'd like to get started!
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
