mathlib

9f9015c6 - refactor(category_theory/sites/*): Redefine the category of sheaves. (#10678)

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](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Redefining.20Sheaves/near/263308542)