Commit 2026-02-05 21:16 a16e0e92

feat(CategoryTheory/Sites): characterization of (pre)stacks for a precoverage (#33256) When a precoverage J satisfies slightly stronger axioms than those of pretopologies, then in order to verify that a pseudofunctor is a prestack (resp. a stack), it suffices to check that the toDescentData functors attached to presieves in J are fully faithful (resp. equivalences).