Def CategoryTheory.Limits.fiberwiseColimit

Modification history

2024-11-03 13:44

Mathlib/CategoryTheory/Limits/Shapes/Grothendieck.lean

feat(CategoryTheory): Colimits on the Grothendieck construction (#18442) …

Added CategoryTheory.Limits.fiberwiseColimit View on Github →