feat(category_theory): sieves (#3909)
feat(category_theory): sieves (#3909)

Define sieves, from my topos project. Co-authored by @EdAyers. 

These definitions and lemmas have been battle-tested quite a bit so I'm reasonably confident they're workable.





leanprover-community/mathlib,leanprover-community/mathlib