mathlib

3a860cc4 - fixup(category_theory/sites): add arrow sets that aren't sieves (#4703)

fixup(category_theory/sites): add arrow sets that aren't sieves (#4703) Broken off from #4648. - I realised that by creating a type `arrows_with_codomain` I can avoid using `set (over X)` entirely (the bit I was missing was that `derive complete_lattice` works on the new type even though it wasn't inferred on the pi-type), so I changed sieves to use that instead. - I added constructors for special arrow sets. The definitions of `singleton_arrow` and `pullback_arrows` look a bit dubious because of the equality and `eq_to_hom` stuff; I don't love that either so if there's a suggestion on how to achieve the same things (in particular stating (1) and (3) from: https://stacks.math.columbia.edu/tag/00VH, as well as a complete lattice structure) I'd be happy to consider. - I added a coercion so we can write `S f` instead of `S.arrows f` for sieves.