Commit 2025-12-11 16:28 d76e5324

View on Github →

feat(CategoryTheory): combine pullback cones in the functor category (#32618)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean

added def CategoryTheory.Limits.PullbackCone.combine

added def CategoryTheory.Limits.PullbackCone.combineIsLimit

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean

added def CategoryTheory.Limits.cospanHomMk

added def CategoryTheory.Limits.cospanIsoMk

added def CategoryTheory.Limits.spanHomMk

added def CategoryTheory.Limits.spanIsoMk