Def CategoryTheory.Limits.Cofan.isColimitOfIsIsoSigmaDesc

Modification history

2023-11-14 07:28

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

feat(CategoryTheory): a presheaf preserves certain products iff it `IsSheafFor` certain presieves (#7804) …

Added CategoryTheory.Limits.Cofan.isColimitOfIsIsoSigmaDesc View on Github →