Commit 2020-10-21 01:39 3a860cc4

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.