Commit 2020-08-15 12:43 099f070f

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!