Commit 2020-12-10 13:59 12d097e3

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