mathlib3

73f119e0 - refactor(category_theory/pairwise): change direction of morphisms in the category of pairwise intersections (#4537)

refactor(category_theory/pairwise): change direction of morphisms in the category of pairwise intersections (#4537) Even though this makes some proofs slightly more awkward, this is the more natural definition. In a subsequent PR about another equivalent sheaf condition, it also makes proofs less awkward, too! Co-authored-by: Scott Morrison <scott.morrison@gmail.com>