Commit 2022-02-07 19:33 9ceb3c2a

feat(topology/sheaf_condition): connect sheaves on sites and on spaces without has_products (#11706) As an application of #11692, show that the is_sheaf_opens_le_cover sheaf condition on spaces is equivalent to is_sheaf on sites, thereby connecting sheaves on sites and on spaces without the value category has_products for the first time. (@justus-springer: you might want to take a look so as to determine whether and which of your work in #9609 should be deprecated.) This could be seen as a step towards refactoring sheaves on spaces through sheaves on sites.

• depends on: #11692