Commit 2021-12-16 21:36 9f9015c6
View on Github →refactor(category_theory/sites/*): Redefine the category of sheaves. (#10678) This refactor redefines sheaves and morphisms of sheaves using bespoke structures. This is an attempt to make automation more useful when dealing with categories of sheaves. See the associated zulip discussion