Commit 2023-11-20 16:56 1fe92bf7

feat(CategoryTheory): finite-product preserving presheaves are sheaves for extensive presieves (#7949) We prove that finite-product preserving presheaves on extensive categories are sheaves for extensive presieves.

• depends on: #7804