mathlib3

12d097e3 - feat(category_theory/sites/sieves): change presieve operation defs (#5295)

feat(category_theory/sites/sieves): change presieve operation defs (#5295) change the definitions of operations on presieves to avoid `eq_to_hom` and use inductive types instead, which makes proofs a lot nicer