Commit 2024-06-09 22:38 6a42b427

feat(CategoryTheory/Sites): transfer WEqualsLocallyBijective (#13632) Under certains conditions on a functor between sites (D, K) to (C, J), we express the class J.W of morphisms of presheaves which become iso after sheafification as the inverse image of the class K.W. We deduce that the typeclass WEqualsLocallyBijective can be transported from (D, K) to (C, J).