Def CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit

Modification history

2024-11-03 13:44

Mathlib/CategoryTheory/Limits/Shapes/Grothendieck.lean

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

Added CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit View on Github →